prim_variant

Term.prim_variant : term list -> term -> term

Rename a variable to be different from any in a list.

The function prim_variant is exactly the same as variant, except that it doesn’t rename away from constants.

Failure

prim_variant l t fails if any term in the list l is not a variable or if t is not a variable.

Example

> variant [] (mk_var("T",bool));
val it = “T'”: term

> prim_variant [] (mk_var("T",bool));
val it = “T”: term

Comments

The extra amount of renaming that variant does is useful when generating new constant names (even though it returns a variable) inside high-level definition mechanisms. Otherwise, prim_variant seems preferable.

See also

Term.variant, Term.mk_var, Term.genvar, Term.mk_primed_var