Agda.TypeChecking.Injectivity
- reduceHead :: Term -> TCM (Blocked Term)
- headSymbol :: Term -> TCM (Maybe TermHead)
- checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
- functionInverse :: Term -> TCM InvView
- data InvView
- useInjectivity :: Comparison -> Type -> Term -> Term -> TCM Constraints
Documentation
reduceHead :: Term -> TCM (Blocked Term)
Reduce simple (single clause) definitions.
headSymbol :: Term -> TCM (Maybe TermHead)
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
functionInverse :: Term -> TCM InvView
Argument should be on weak head normal form.
useInjectivity :: Comparison -> Type -> Term -> Term -> TCM Constraints