Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 FunctionInverseSource
functionInverse :: Term -> TCM InvViewSource
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 ConstraintsSource
Produced by Haddock version 2.6.1