Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Injectivity

Synopsis

Documentation

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

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

functionInverse :: Term -> TCM InvView Source #

Argument should be in weak head normal form.

data InvView Source #

Constructors

Inv QName [Elim] (Map TermHead Clause) 
NoInv 

data MaybeAbort Source #

Constructors

Abort 
KeepGoing 

useInjectivity :: Comparison -> Type -> Term -> Term -> TCM () Source #