mk_const : string * hol_type -> term
(A type ty1 is an ’instance’ of a type ty2 when match_type ty2 ty1 does not fail.)
Note, however, that constants with the same name (and type) may be declared in different theories. If two theories having constants with the same name n are in the ancestry of the current theory, then mk_const(n,ty) will issue a warning before arbitrarily selecting which constant to construct. In such situations, mk_thy_const allows one to specify exactly which constant to use.
- mk_const ("T", bool); > val it = `T` : term - mk_const ("=", bool --> bool --> bool); > val it = `$=` : term - try mk_const ("test", bool); Exception raised at Term.mk_const: test not found
The following example shows a new constant being introduced that has the same name as the standard equality of HOL. Then we attempt to make an instance of that constant.
- new_constant ("=", bool --> bool --> bool); > val it = () : unit - mk_const("=", bool --> bool --> bool); <<HOL warning: Term.mk_const: "=": more than one possibility>> > val it = `$=` : term