Proof assistant for the λΠ-calculus modulo rewriting
Library lambdapi.core
Module Core . Tree_type . TC
type t =
| Symb of Common.Path.t * string * int(*

Symbol identified by a fully qualified name (module path and name) and its arity in the pattern.

| Vari of int(*

A bound variable identified by a (branch-wise) unique integer. These variables are used with a bidirectional map (implemented as two maps) to a higher order (Bindlib) variable. They are also used in the environment builder to refer to the higher order variables a term may depend on.


Atomic pattern constructor. Term are identified by these constructors in the trees. During matching (in Eval.tree_walk), terms are transformed into these constructors to get the right sub-tree.

NOTE the effective arity carried by the representation of a symbol is specific to a given symbol instance. Indeed, a symbol (in the sense of Term.sym) may lead to several constructors, with different effective arities. In the pattern “f g (g $x)” for example, symbol g is used with arity 0 (first occurence) and 1 (second occurence).

val pp : t Lplib.Base.pp

pp oc c prints tree constructor c to output channel o.

val compare : t -> t -> int

compare c1 c2 implements a total order on constructors.