Term.mk_const

STRUCTURE

SYNOPSIS

Constructs a constant.

DESCRIPTION

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);
   <<HOL warning: Term.mk_const: "=": more than one possibility>>

   > val it = `$=` : term

SEEALSO

mk_thy_const, dest_const, is_const, mk_var, mk_comb, mk_abs, match_type