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''.