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

• raises [Not_found]

  otherwise.

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

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.

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.

to_map builds a map from a context.

names c returns the set of names in c.

fresh c id returns a string starting with id and not in c.