| 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
| Functor (AffineHole r) Source # | |
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) Source # | |
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 # | |