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

Safe HaskellNone

Agda.TypeChecking.Injectivity

Synopsis

Documentation

reduceHead :: Term -> TCM (Blocked Term)

Reduce simple (single clause) definitions.

functionInverse :: Term -> TCM InvView

Argument should be on weak head normal form.

data InvView

Constructors

Inv QName Args (Map TermHead Clause) 
NoInv