Proof assistant for the λΠ-calculus modulo rewriting
Library lambdapi.core
Module Core . LibMeta
val meta_counter : int ref
val reset_meta_counter : unit -> unit

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

val fresh : Term.problem -> Term.term -> int -> Term.meta

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.

val fresh_box : Term.problem -> Term.tbox -> int -> Term.meta

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.

val set : Term.problem -> Term.meta -> Term.tmbinder -> unit

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 named ?name (if provided) 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.

val make_codomain : Term.problem -> Term.ctxt -> Term.term -> Term.tbinder

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.

val iter : bool -> ( Term.meta -> unit ) -> Term.ctxt -> Term.term -> unit

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.

val occurs : Term.meta -> Term.ctxt -> Term.term -> bool

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