package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/lambdapi.core/Core/Ctxt/index.html
Module Core.Ctxt
Source
Typing context.
type_of x ctx
returns the type of x
in the context ctx
when it appears in it, and
def_of x ctx
returns the definition of x
in the context ctx
if it appears, and None
otherwise
mem x ctx
tells whether variable x
is mapped in the context ctx
.
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.
to_prod_box bctx t
is similar to to_prod bctx t
but operates on boxed contexts and terms.
box_context ctx
lifts context ctx
to a boxed context.
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
.
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
.
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.