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.

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.

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.