reset_meta_counter () resets the counter used to produce meta keys.

fresh p ?name a n creates a fresh metavariable of type a and arity n with the optional name name, and adds it to p.

fresh_box p a n is the boxed counterpart of fresh_meta. It is only useful in the rare cases where the type of a metavariable contains a free term variable environment. This should only happens when scoping the rewriting rules, use this function with care. The metavariable is created immediately with a dummy type, and the type becomes valid at unboxing. The boxed metavariable should be unboxed at most once, otherwise its type may be rendered invalid in some contexts.

set p m v sets the metavariable m of p to v. WARNING: No specific check is performed, so this function may lead to cyclic terms. To use with care.

make p ctx a creates a fresh metavariable term of type a in the context ctx, and adds it to p.

bmake p bctx a is the boxed version of make: it creates a fresh boxed metavariable in boxed context bctx of boxed type a. It is the same as lift (make p c b) (provided that bctx is boxed c and a is boxed b), but more efficient.

make_codomain p ctx a creates a fresh metavariable term of type Type in the context ctx extended with a fresh variable of type a, and updates p with generated metavariables.

bmake_codomain p bctx a is make_codomain p bctx a but on boxed terms.

iter b f c t applies the function f to every metavariable of t and, if x is a variable of t mapped to v in the context c, then to every metavariable of v, and to the type of every metavariable recursively if b is true.

occurs m c t tests whether the metavariable m occurs in the term t when variables defined in the context c are unfolded.