next up previous contents
Next: Theorem Display Commands Up: Appendix: Reference for Individual Previous: Movement Commands

Declaration Commands

showdec
``showdec term'' displays the declaration information for the constant or operator ``term''. (relative types of left and right subterms and default left subterm if used as a prefix). (walk command ``''). Displays comments.

showalldecs
Shows all declarations, one per keystroke on Enter. Use any key other than Enter to break out.

declaretypedinfix
``declaretypedinfix left-type right-type name'' declares the operator ``name'' with left and right types ``left-type'' and ``right-type'' (the types are integers without double quotes; negative integers are prefixed with ĩn ML). (walk command ``Y'').

declareconstant
``declareconstant name'' declares a constant with name ``name''. (walk command ``c'').

declareinfix
``declareinfix name'' declares a type-level operator (both relative types 0) called ``name''. (walk command ``d'').

declareunary
``declareunary name'' declares a type-level operator called ``name'' usable as a prefix with default left subterm defaultprefix. (walk command ``1'').

newcomment
``newcomment name comment'' attaches the comment ``comment'' to the declared object named by ``name''. This supersedes older comments.

appendcomment
As newcomment, except that comments are appended to previous comments.

makeunary
``makeunary name'' assigns the default left argument ``defaultprefix'' to an operator which may already exist (it does not attempt a declaration).

declareopaque
``declareopaque infix'' causes the operator ``infix'' to be treated as referentially opaque for purposes of abstraction. (walk command ``y'') New restriction: this command can be used only to introduce a new operator; previously existing operators cannot be made opaque.

makescin, makescout
``makescin name theorem'' causes the function constant or operator named by ``name'' to be declared as having input (resp. output) restricted to absolute types (strongly Cantorian sets) with consequent weakening of stratification requirements. The theorem named by ``theorem'' must witness this fact.

declarepretheorem
``declarepretheorem thm'' reserves ``thm'' as the name of a future theorem (needed for the proofs of recursive tactics). (walk command ``P'').

forget
``forget name'' eliminates declarations of all theorems which depend on or refer to theorem ``name''. It will eliminate an entire module if any component depends on ``name''.


next up previous contents
Next: Theorem Display Commands Up: Appendix: Reference for Individual Previous: Movement Commands

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