| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Injectivity

Synopsis

reduceHead :: Term -> TCM (Blocked Term)
headSymbol :: Term -> TCM (Maybe TermHead)
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
functionInverse :: Term -> TCM InvView

data InvView

= Inv QName Args (Map TermHead Clause)
| NoInv

useInjectivity :: Comparison -> Type -> Term -> Term -> TCM Constraints

Documentation

reduceHead :: Term -> TCM (Blocked Term) | Source

Reduce simple (single clause) definitions.

headSymbol :: Term -> TCM (Maybe TermHead) | Source

checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse | Source

functionInverse :: Term -> TCM InvView | Source

Argument should be on weak head normal form.

data InvView | Source

Constructors

Inv QName Args (Map TermHead Clause) |
NoInv |

useInjectivity :: Comparison -> Type -> Term -> Term -> TCM Constraints | Source

Produced by Haddock version 2.4.2