new_constant

Theory.new_constant : string * hol_type -> unit

Declares a new constant in the current theory.

A call new_constant(n,ty) installs a new constant named n in the current theory. Note that new_constant does not specify a value for the constant, just a name and type. The constant may have a polymorphic type, which can be used in arbitrary instantiations.

Failure

Never fails, but issues a warning if the name is not a valid constant name. It will overwrite an existing constant with the same name in the current theory.

See also

Theory.constants, boolSyntax.new_infix, boolSyntax.new_binder, Definition.new_definition, Definition.new_type_definition, Definition.new_specification, Theory.new_axiom, boolSyntax.new_infixl_definition, boolSyntax.new_infixr_definition, boolSyntax.new_binder_definition