mk_var

Term.mk_var : string * hol_type -> term

Constructs a variable of given name and type.

If v is a string and ty is a HOL type, then mk_var(v, ty) returns a HOL variable.

Failure

Never fails.

Comments

mk_var can be used to construct variables with names which are not acceptable to the term parser. In particular, a variable with the name of a known constant can be constructed using mk_var.

See also

Term.dest_var, Term.is_var, Term.mk_const, Term.mk_comb, Term.mk_abs