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