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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Injectivity

Synopsis

Documentation

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