Module Core.LibMetaSource

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 ?name 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.

name m returns a string representation of m.

of_name p n returns Some m if m is an element of the set of metas of p with name n, and None otherwise.

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

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.

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.