next up previous contents
Next: Rule Introduction Commands Up: Appendix: Reference for Individual Previous: Editing Commands

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.



Randall Holmes
Fri Sep 5 16:28:58 MDT 1997