Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

Contexts with at most one hole.

# Documentation

data AffineHole r a Source #

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 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 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 # |