---------------------------------------------------------------------- mk_const (Term) ---------------------------------------------------------------------- mk_const : string * hol_type -> term SYNOPSIS Constructs a constant. DESCRIBE If {n} is a string that has been previously declared to be a constant with type {ty} and {ty1} is an instance of {ty}, then {mk_const(n,ty1)} returns the specified instance of the constant. (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. FAILURE Fails if {n} is not the name of a known constant, or if {ty} is not an instance of the type that the constant has in the signature. EXAMPLE - 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); <