Registering and checking builtin symbols.

Typing context.

Scoping environment for variables.

Evaluation and conversion.

Define a ghost signature that contain symbols used by the kernel but not defined by the user.

Type inference and checking

Compute the inverse image of a term wrt an injective function.

Functions to manipulate metavariables.

Basic operations on terms.

Pretty-printing for the core AST.

Signature state.

Signature for symbols.

Internal representation of terms.

Compilation of rewriting rules to decision trees.

Miscellaneous types and utilities for decision trees.

Solving unification constraints.

Symbols and signature for unification rules.

Version informations.