mk_var : string * hol_type -> term
- SYNOPSIS
-
Constructs a variable of given name and type.
- DESCRIPTION
-
mk_var("var",`:ty`) returns the variable `var:ty`.
- FAILURE CONDITIONS
-
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
-
dest_var, is_var, mk_const, mk_comb, mk_abs.