next up previous contents
Next: Tutorial Up: Command Reference Previous: The Logic of the

List of Error Messages

This may not be entirely up to date.

Division by zero!
Message from built in arithmetic with obvious meaning.

At beginning, At end
Messages from the scan command sent when you try to read before the first entry or after the last entry in a tree.

<return> to view,l to go left, r to go right, q to quit
Sent by the scan command when an inappropriate letter is entered.

No negative precedence
The setprecedence command does not permit negative precedence to be set.

Errors found in displayed term
This message is issued by the term display command when it encounters the error term Constant "".

Warning: adding leading parenthesis
This warning is issued by the parser when it is forced to add a leading parenthesis to make sense of a term.

Subterm error
This message is issued by the movement commands when one attempts to move to a subterm of an atomic term.

Ill-formed hypothesis, Ill-formed case expression
These messages are issued by the declaration checking function when it encounters inapprorpaite uses of |-| or case expressions without a pair of alternatives as the second argument, respectively.

Illegal opacity declaration
Issued by the commands for declaring opaque operators when they do not succeed. Possible reasons include ill-formed operator names, conflicts with previous declarations.

Undeclared constants or embedded theorems present
Issued by a declaration checking function of the prover when it finds a term unacceptable, usually because it contains undeclared constants or operators or was so ill-formed as to be impossible to parse.

Meaningless bound variable or unstratified abstraction error
Issued by a declaration checking function when it finds errors in stratification or in indexing of deBruijn levels (variable binding) in a term.

Illegal or repeated constant declaration of, Illegal or repeated infix declaration of
(it will supply the declared object). Issued by the declaration commands when a declaration is illegal or such an object has already been declared. These messages will normally be issued many times during theorem export.

Name already in use
Issued by declareopaque when an attempt is made to redeclare a preexisting constant.

Not an infix
Issued by declareopaque when a non-infix parameter is provided.

Constant is a numeral
Issued by showdec when one attempts to show declaration of a numeral (numerals are ``predeclared'').

Opaque infix variable
Issued by showdec when one attempts to show declaration of an operator variable declared as opaque.

Constant not found
Issued by showdec when no constant with the given name is found.

Theorem not found
Issued by thmdisplay when there is no such theorem. Also used by reprove.

Built-in operation
Issued by thmdisplay when one attempts to display a ``theorem'' which is actually a hard-wired tactic.

No definition found
Issued by seedef when no such defined notion is found.

Program not found
Issued by seeprogram when no program is bound to the given operator or function (or when the operator or function itself is not understood).

Not an equation!
Issued by commands which match theorems when the object presented to match with theorems is not an equation.

No such theorem
Issued by showmatchthm when no matching theorem is found. Also issued by applythm and applyconvthm when they do not recognize their arguments.

Illegal theorem declaration
Issued by axiom when parsing or declaration problems prevent an axiom from being accepted.

Stratification, opacity or impredicativity error in definition
Issued by the defineconstant command when stratification or related considerations prevent a definition from being accepted.

Declaration or syntax error in definition
Issued by the defineconstant command when undeclared objects appear or there are parsing problems; this includes the case of circular definitions.

Stratification or opacity error in infix definition
Issued by infix definition commands when stratification-related considerations cause a definition to be rejected.

Warning: automatically declaring default left argument of defined prefix
Issued by infix definition commands when an operator is implicitly defined as unary.

Declaration or syntax error in infix declaration
Issued by infix definition commands when undeclared objects or syntax errors appear in a definition. This includes attempts at circular definition.

Argument is not defined appropriately
Issued by the undefine command when the object supplied to be ``undefined'' was not defined in the first place.

Inappropriate argument
Issued by the defineprimitive command when it is given an unsuitable theorem or a non-theorem.

Definition format error
Issued by defineprimitive when it is given a theorem which does not have the form of a definition.

Not a theorem
Issued by makeanaxiom when the argument is not a theorem.

Not applicable to definitions, Not applicable to built-in theorems
Issued by makeanaxiom when argument is a definition or a built-in theorem.

Illegal pretheorem declaration
Issued by declarepretheorem when syntax or declaration errors cause it to reject a declaration.

Theorem is not of right form
Issued by proveprogram when theorem is not of the correct form to be bound to the given function or operator.

Impossible error in program declaration
This error message should never be issued by proveprogram, barring bugs.

Undeclared object error or program already present
Issued by proveprogram when object is undeclared or already has a program bound to it.

Deprogram what???!
Issued by deprogram when it does not recognize its argument.

No program to delete or change
Issued by deprogram when there is no program to remove.

At top already
Warning issued by the up command when one attempts to go up from the top of a parse tree.

No such hypothesis
Issued by lookhyp when its argument is inappropriate.

Bad environment name or corrupt environment
Issued by saveenv or backupenv when an attempt is made to save or back up a corrupt environment or to save an environment with an ill-formed name. Warning: the message will appear when a perfectly good new term is started if the previous environment was corrupt, due to the automatic attempt to back up the bad environment.

Reconstructing environment from theory
Remark made by getenv when it is loading an environment from a saved theory into the local data structure which stores environments.

Environment not found
Issued by getenv when it finds no environment named by the argument.

Cannot drop backup
Issued by dropenv when it is told to drop the current backup environment.

No match found
Issued by upto and related commands when no matching term is found to which to move.

Invalid argument
Issued by upto and related commands when the argument doesn't pass a declaration check (or doesn't parse).

What theorem??!!
Issued by commands like uptols when argument is not recognized as a theorem.

Built in theorem not supported by apply(conv)thm
Issued by applythm and applyconvthm when they encounter built-in theorems which they do not support.

No such environment
Issued by applyenv, applyconvenv when argument is not recognized.

Corrupt environment
Issued by applyenv, applyconvenv when rerenced environment is corrupt (this actually should not happen).

Undeclared constants in theorem to be proved
Issued by prove when theorem does not pass a declaration check. This may signal stratification errors as well as declaration errors.

Conflict with existing theorem name (or illegal name or format)
Issued by prove when it objects to the proposed name or format of a theorem.

Environment name not appropriate
Issued when an attempt is made to use autoprove when there is not a user-defined environment name.

Cannot modify an axiom
, Cannot modify a definition Issued by reprove when an attempt is made to modify an axiom or definition.

Introduces additional dependencies
Issued by reprove when it rejects a change in a theorem because it strengthens dependencies.

This command can only be issued at top of term
Issued by interaxiom when an attempt is made to interpret a proper subterm as an axiom.

Current subterm is not of correct form
Issued by interaxiom when the current subterm is not an equation.

Target is not an axiom, is a definition, or does not match environment
The all-purpose error message of proveanaxiom.

Incorrect new name for old definition
Issued by redefineconstant when declaration collisions or syntax make the proposed new name for the old definition inappropriate.

Source is not a suitable definition
Issued by redefineconstant when it does not like the proposed new definition.

Declaration or syntax error in redefinition
Issued by redefineconstant probably only when the proposed new definition would be circular.

Inappropriate arguments
Issued by redefineinfix for a variety of offenses against declarations.

Stratification or opacity error in infix redefinition
Issued by redefineinfix when stratification or related considerations cause new definition to be rejected.

Declaration or syntax error in infix redeclaration
Issued by redefineinfix probably only when definition would be circular.

Illegal substitution attempted
Issued by assign and relatives when bad substitutions are attempted.

No rule to drop!
Issued by droprule when it is invoked inappropriately.

No rule to toggle
Issued by altrule when it is invoked inappropriately.

Theorem or pretheorem not found
Issued by ruleintro when it does not recognize its argument as a theorem.

Ill-formed theorem name
Issued by ruleintro when it cannot parse its argument to find a theorem name.

Declaration error
Issued by ruleintro when its argument contains undeclared constants or cannot be parsed at all.

No matching theorem found
Issued by matchruleintro or targetruleintro when it cannot find a matching theorem to introduce.

Bad arithmetic evaluation
Internal error - I doubt that the prover can actually issue it to a user.

No such theory to get
Issued by gettheory when it does not understand its argument.

Won't drop backup of current theory
Issued by droptheory when it declines to drop the current backup.

No such theory found to drop
Issued by droptheory when it does not understand its argument.

View of that name already exists
Issued by declareview in event of name collision.

No such constant to project
Issued by viewasin when it does not understand its local declaration argument.

Cannot export infix without its definition
Issued by viewasin when an attempt is made to export a defined operator without its definition.

Already found in view
Issued by viewasin when there is already a binding in the view.

Such an item is not found in such a view
The all-purpose errormessage of dropfromview.

No such view to drop
Issued when dropaview does not understand its argument.

No such view
Used by viewasin, viewofin, showview, or a theorem export command when it does not recognize its view argument.

No such item in view
Used by viewofin when it does not recognize its binding argument.

Bad deps in export list
An error in theorem export. The theorem(s) to be exported depend on axioms not found in the view to be used.

Constant in view is not declared
An error in theorem export. A constant in the view is not declared.

Constant definition matching error,Defined infix matching error
An error in theorem export. A definition does not match.

Missing declarations in target
An error in theorem export. Something the view leads one to expect is not present in the target theory.

Infix typing error
An error in theorem export. The types of an operator do not match correctly.

No such remote theory
Theorem export command does not recognize the target theory.

Construction of export list failed
An error in theorem export. Export list could not be constructed.

Predicativity error in export
An error in theorem export. Source theory is impredicative and target theory is predicative.

Opacity error in export
An error in theorem export. Something in target theory is opaque and its counterpart in source is not.

Theory match failure
An error in theorem export. Source and target theories do not match as claimed by the view.

Export aborted; theory restored
Remark issued on backtracking from a failed theorem export.

Illegal character command
Message from the walk interface when it does not recognize a command.

Unknown or inappropriate theorem(s)
Message from the pushtheorem or poptheorem commands when given inappropriate arguments; the forget command sends a similar message (in the singular).


next up previous contents
Next: Tutorial Up: Command Reference Previous: The Logic of the

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