lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.
ON THIS PAGE
No table of contents