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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Injectivity

Synopsis

Documentation

functionInverse :: Term -> TCM InvView

Argument should be in weak head normal form.

data InvView

Constructors

Inv QName [Elim] (Map TermHead Clause) 
NoInv