package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

doc/lambdapi.core/Core/Ctxt/index.html

Module Core.CtxtSource

Typing context.

Sourceval type_of : Term.tvar -> Term.ctxt -> Term.term

type_of x ctx returns the type of x in the context ctx when it appears in it, and

  • raises [Not_found]

    otherwise.

Sourceval def_of : Term.tvar -> Term.ctxt -> Term.ctxt * Term.term option

def_of x ctx returns the definition of x in the context ctx if it appears, and None otherwise

Sourceval mem : Term.tvar -> Term.ctxt -> bool

mem x ctx tells whether variable x is mapped in the context ctx.

Sourceval to_prod : Term.ctxt -> Term.term -> Term.term * int

to_prod ctx t builds a product by abstracting over the context ctx, in the term t. It returns the number of products as well.

Sourceval to_prod_box : Term.bctxt -> Term.tbox -> Term.tbox * int

to_prod_box bctx t is similar to to_prod bctx t but operates on boxed contexts and terms.

Sourceval box_context : Term.ctxt -> Term.bctxt

box_context ctx lifts context ctx to a boxed context.

Sourceval to_abst : Term.ctxt -> Term.term -> Term.term

to_abst ctx t builds a sequence of abstractions over the context ctx, in the term t.

to_let ctx t adds the defined variables of ctx on top of t.

Sourceval sub : Term.ctxt -> Term.tvar array -> Term.ctxt

sub ctx vs returns the sub-context of ctx made of the variables of vs.

unfold ctx t behaves like Term.unfold unless term t is of the form Vari(x) with x defined in ctx. In this case, t is replaced by the definition of x in ctx. In particular, if no operation is carried out on t, we have unfold ctx t == t.

Sourceval get_args : Term.ctxt -> Term.term -> Term.term * Term.term list

get_args ctx t decomposes term t as Term.get_args does, but any variable encountered is replaced by its definition in ctx (if it exists).

to_map builds a map from a context.

OCaml

Innovation. Community. Security.