abs package:Agda

Binder. Abs: The bound variable might appear in the body. NoAbs is pseudo-binder, it does not introduce a fresh variable, similar to the const of Haskell.
The body has (at least) one free variable. Danger: unAbs doesn't shift variables properly
Absurd lambdas are internally represented as identity with variable name "()".
Make an absurd pattern with the given de Bruijn index.
Followed by possibly a final absurd pattern.
subst j u . absTerm j u == id
abstractType r a v b[v] = b where a : v.
Name of absurdLambda definitions.