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

Agda.TypeChecking.Injectivity

Synopsis

Documentation

reduceHead :: Term -> TCM (Blocked Term)Source

Reduce simple (single clause) definitions.

functionInverse :: Term -> TCM InvViewSource

Argument should be on weak head normal form.