prim_mk_const

Term.prim_mk_const : {Thy:string, Name:string} -> term

Build a constant.

If Name is the name of a previously declared constant in theory Thy, then prim_mk_const {Thy,Name} will return the specified constant.

Failure

If Name is not the name of a constant declared in theory Thy.

Example

> prim_mk_const {Thy="min", Name="="};
val it = “$=”: term

> type_of it;
val it = “:α -> α -> bool”: hol_type

Comments

The difference between mk_thy_const (and mk_const) and prim_mk_const is that mk_thy_const and mk_const will create type instances of polymorphic constants, while prim_mk_const merely returns the originally declared constant.

See also

Term.mk_thy_const