lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library lambdapi.core
Module Core
module Builtin : sig ... end

Registering and checking builtin symbols.

module Ctxt : sig ... end

Typing context.

module Env : sig ... end

Scoping environment for variables.

module Eval : sig ... end

Evaluation and conversion.

module Infer : sig ... end

Type inference and checking

module Inverse : sig ... end

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

module LibMeta : sig ... end

Functions to manipulate metavariables.

module LibTerm : sig ... end

Basic operations on terms.

module Print : sig ... end

Pretty-printing for the core AST.

module Sig_state : sig ... end

Signature state.

module Sign : sig ... end

Signature for symbols.

module Term : sig ... end

Internal representation of terms.

module Tree : sig ... end

Compilation of rewriting rules to decision trees.

module Tree_type : sig ... end

Miscellaneous types and utilities for decision trees.

module Unif : sig ... end

Solving unification constraints.

module Unif_rule : sig ... end

Symbols and signature for unification rules.

module Version : sig ... end

Version informations.