Agda.Utils.AffineHole

Contexts with at most one hole.

Documentation

data AffineHole r a

Constructors

ZeroHoles a

A constant term.

OneHole (r -> a) r

A term with one hole and the (old) contents.

ManyHoles

A term with many holes (error value).

Instances

Functor (AffineHole r)

Defined in Agda.Utils.AffineHole

Methods

fmap :: (a -> b) -> AffineHole r a -> AffineHole r b

(<$) :: a -> AffineHole r b -> AffineHole r a

Applicative (AffineHole r)

Defined in Agda.Utils.AffineHole

Methods

pure :: a -> AffineHole r a

(<*>) :: AffineHole r (a -> b) -> AffineHole r a -> AffineHole r b

liftA2 :: (a -> b -> c) -> AffineHole r a -> AffineHole r b -> AffineHole r c

(*>) :: AffineHole r a -> AffineHole r b -> AffineHole r b

(<*) :: AffineHole r a -> AffineHole r b -> AffineHole r a