Documentation

Type of scope-safe \(\lambda\Pi\)-terms with pairs.

Patterns.

Check if a name in the extended context is introduced in a pattern or comes from the outer scope n.

This is a generalization of unsinkName to Pattern.

Default way to print a name using its internal Id.

Pretty-print a \(\lambda\Pi\)-term directly (without converting to raw term).

>>> ppExpr identity
"\955x0. x0"
>>> ppExpr (churchN 2)
"\955x0. \955x1. x0 (x0 (x1))"

Pretty-print a pattern in a \(\lambda\Pi\)-term (without converting to raw pattern)..

Pretty-print a closed scode-safe \(\lambda\Pi\)-term using BNFC-generated printer (via Term).

Extend scope with variables inside a pattern. This is a more flexible version of extendScope.

Refresh (if needed) bound variables introduced in a pattern. This is a more flexible version of withRefreshed.

Refresh (if needed) bound variables introduced in a pattern. This is a more flexible version of withRefreshed.

Refresh (if needed) bound variables introduced in a pattern.

This is a version of withRefreshedPattern that uses functional renamings instead of Substitution.

Perform substitution in a \(\lambda\Pi\)-term.

Perform substitution in a \(\lambda\Pi\)-term and normalize binders in the process.

Convert a raw pattern into a scope-safe one.

Convert a scope-safe pattern into a raw pattern.

Convert a scope-safe term into a raw term.

Convert a closed scope-safe term into a raw term.

Convert a scope-safe pattern into a raw pattern converting raw identifiers directly into VarIdent

Convert a scope-safe term into a raw term converting raw identifiers directly into VarIdent.

Convert a raw term into a scope-safe \(\lambda\Pi\)-term.

Convert a raw term into a closed scope-safe term.

Match a pattern against an expression.

Compute weak head normal form (WHNF).

>>> whnf emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)"
λ x0 . λ x1 . x1

>>> whnf emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))"
λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1)

Note that during computation bound variables can become unordered in the sense that binders may easily repeat or decrease. For example, in the following expression, inner binder has lower index that the outer one:

>>> whnf emptyScope "(λx.λy.x)(λx.x)"
λ x1 . λ x0 . x0

At the same time, without substitution, we get regular, increasing binder indices:

>>> "λx.λy.y" :: Expr VoidS
λ x0 . λ x1 . x1

To compare terms for \(\alpha\)-equivalence, we may use alphaEquiv:

>>> alphaEquiv emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y"
True

We may also normalize binders using refreshExpr:

>>> refreshExpr emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)")
λ x0 . λ x1 . x1

Normalize all binder identifiers in an expression.

\(\alpha\)-equivalence check for two terms in one scope via normalization of bound identifiers (via refreshExpr).

This function may perform some unnecessary changes of bound variables when the binders are the same on both sides.

Unsafely check for equality of two Patterns.

This does not include \(\alpha\)-equivalence!

Unsafely check for equality of two Exprs.

This does not include \(\alpha\)-equivalence!

Interpret a λΠ command.

Interpret a λΠ program.

Default interpreter program. Reads a λΠ program from the standard input and runs the commands.

A helper for constructing \(\lambda\)-abstractions.

An identity function as a \(\lambda\)-term:

>>> identity
λ x0 . x0

Church-encoding of a natural number \(n\).

>>> churchN 0
λ x0 . λ x1 . x1

>>> churchN 3
λ x0 . λ x1 . x0 (x0 (x0 x1))