= 768" x-on:close-sidebar="sidebar=window.innerWidth >= 768 && true">
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
lambdapi 2.2.0
Libraries
This package provides the following libraries (via dune):
lambdapi.common
Documentation:
Common.Console
Verbose level and loggers management.Common.Debug
Helper functions for debugging. *Common.Error
Warnings and errors.Common.Escape
Escaped identifiers"{|...|}"
.Common.Library
Lambdapi library management.Common.Logger
Functions for creating loggers. *Common.Path
Module paths in the Lambdapi library.Common.Pos
Positions in Lambdapi files.
Dependencies: timed, lambdapi.lplib
lambdapi.core
Documentation:
Core.Builtin
Registering and checking builtin symbols.Core.Ctxt
Typing context.Core.Env
Scoping environment for variables.Core.Eval
Evaluation and conversion.Core.Infer
Type inference and checkingCore.Inverse
Compute the inverse image of a term wrt an injective function.Core.LibMeta
Functions to manipulate metavariables.Core.LibTerm
Basic operations on terms.Core.Print
Pretty-printing for the core AST.Core.Sig_state
Signature state.Core.Sign
Signature for symbols.Core.Term
Internal representation of terms.Core.Tree
Compilation of rewriting rules to decision trees.Core.Tree_type
Miscellaneous types and utilities for decision trees.Core.Unif
Solving unification constraints.Core.Unif_rule
Symbols and signature for unification rules.Core.Version
Version informations.
Dependencies: lambdapi.common, lambdapi.lplib, pratter, bindlib, why3
lambdapi.export
Documentation:
Export.Dk
Export a Lambdapi signature to Dedukti.Export.Hrs
This module provides a function to translate a signature to the HRS format used in the confluence competition.Export.Xtc
This module provides a function to translate a signature to the XTC format used in the termination competition.
Dependencies: lambdapi.core, lambdapi.parsing, lambdapi.lplib
lambdapi.handle
Documentation:
Handle.Command
Handling of commands.Handle.Compile
High-level compilation functions.Handle.Inductive
Generation of induction principles.Handle.Proof
Proofs and tactics.Handle.Query
Handling of queries.Handle.Rewrite
Implementation of the rewrite tactic.Handle.Tactic
Handling of tactics.Handle.Why3_tactic
Calling a prover using Why3.
Dependencies: lambdapi.core, lambdapi.parsing, lambdapi.tool
lambdapi.lplib
Documentation:
Lplib.Array
Lplib.Base
Standard library extension (mostly).Lplib.Color
Lplib.Extra
Lplib.Filename
Lplib.List
Lplib.Option
Lplib.Range
Lplib.RangeMap
Lplib.RangeMap_intf
Lplib.Range_intf
Lplib.String
Dependencies: stdlib-shims, str, unix
lambdapi.lsp
Documentation:
Dependencies: yojson, lambdapi.pure
lambdapi.parsing
Documentation:
Parsing
.DkBasicParsing
.DkLexerParsing
.DkParserParsing
.DkRuleParsing
.DkTokensParsing
.LpLexerParsing
.LpParserParsing
.PackageParsing
.ParserParsing
.PrattParsing
.PrettyParsing
.ScopeParsing
.Syntax
Dependencies: lambdapi.core, menhirLib, pratter, sedlex, sedlex.ppx, lambdapi.common
lambdapi.pure
Documentation: Pure
Dependencies: lambdapi.handle, lambdapi.core
lambdapi.tool
Documentation:
Tool.External
Provides a function for calling external checkers using a Unix command.Tool.Lcr
Incremental verification of local confluenceTool.Sr
Checking that a rule preserves typing (subject reduction property).Tool.Tree_graphviz
Representation of trees as graphviz files.
Dependencies: lambdapi.parsing, lambdapi.core