Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Typing context.
val unbind :
Term.ctxt ->
Term.term ->
Term.term option ->
Term.tbinder ->
Term.tvar * Term.term * Term.ctxtunbind ctx a def b returns a triple (x,t,new_ctx) such that (x,t) is an unbinding of b (in the sense of Bindlib.unbind) and new_ctx is an extension of the context ctx with the declaration that x has type a (only if x occurs in t). If def is of the form Some(u), the context also registers the term u as the definition of variable x.
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_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).