Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

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 Source # (<*>) :: AffineHole r (a -> b) -> AffineHole r a -> AffineHole r b Source # liftA2 :: (a -> b -> c) -> AffineHole r a -> AffineHole r b -> AffineHole r c Source # (*>) :: AffineHole r a -> AffineHole r b -> AffineHole r b Source # (<*) :: AffineHole r a -> AffineHole r b -> AffineHole r a Source #
Functor (AffineHole r) Source # |
Instance details Defined in Agda.Utils.AffineHole Methods fmap :: (a -> b) -> AffineHole r a -> AffineHole r b Source # (<$) :: a -> AffineHole r b -> AffineHole r a Source #