Definition Commands

defineconstant

``defineconstant left-side right-side'', where left-side has the correct format (an undeclared constant possibly applied to lists of parameters) declares the new constant read from ``left-side'' and introduces a theorem with null dependencies of the form ``left-side = right-side'', with the same name as the constant defined.

defineinfix

``defineinfix thm left-side right-side'' where ``left-side'' has a top level undeclared operator (infix or prefix) taking as arguments and possibly applied to parameters or lists of parameters, declares the new operator (as type level) and creates a theorem called ``thm'' equating ``left-side'' and ``right-side''.

definetypedinfix

``definetypedinfix thm left-type right-type left-side right-side'' has the same effect as ``defineinfix thm left-side right-side'', except that the left and right sides of the new operator are assigned relative types ``left-side'' and ``right-side'': these arguments are numerical and are not put in double quotes.

defineitconstant

Like ``defineconstant'', except that the right side is the current subterm.

defineitinfix

Like ``defineinfix'', except that the right side is the current subterm.

defineittypedinfix

Like ``definetypedinfix'', except that the right side is the current subterm.

defineopaque

Defines opaque operators. Same arguments as ``definetypedinfix'', except that types are not needed.