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

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