Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.AffineHole

Description

Contexts with at most one hole.

Documentation

data AffineHole r a Source #

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

Instances details
Applicative (AffineHole r) Source # 
Instance details

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

Functor (AffineHole r) Source # 
Instance details

Defined in Agda.Utils.AffineHole

Methods

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

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