Description of The Mizar Error Messages

Describe the meaning of the Mizar error codes here, post typical or weird examples, suggest changes.

40 most recently changed error messages

Results from Mizar web retrieved at 17:54 (GMT)

Error Number: 190 Mizar Message: Inaccessible theorem Description The theorem used depends on a constructor which is not accessible. To fix, add the missing constructors ...
Error Number: 397 Mizar Message: Term expected Description An off category or unknown symbol appears where a term is expected. Some possible causes include: ...
Error Number: 9 Mizar Message: Too many instantiations Description Please contribute Typical examples environ vocabularies ZFMISC 1, PRE TOPC, EUCLID; constructors ...
Error Number: 93 Mizar Message: Missing field of a prefix Description While giving a definition to the structure one or more fields of the parent structure are omitted ...
Error Number: 856 Mizar Message: Inaccessible requirements directive Description A requirements directive needs prerequisite information that is not being supplied ...
Error Number: 103 Mizar Message: Unknown functor Description The func being used is not defined on the argument type. Some causes of this error are (examples below ...
Error Number: 165 Mizar Message: Unknown functor format Description Seems that this most often means that you do not have the symbol in articles vocabularies. JosefUrban ...
Error Number: 166 Mizar Message: Unknown functor format Description Similar to error 165. A term with argument does not match a known notation a notation directive ...
Error Number: 148 Mizar Message: Unknown private functor Description This can be caused by referencing a function without importing the necessary vocabulary. Importing ...
Error Number: 102 Mizar Message: Unknown predicate Description Some causes of this error are: Omitting a necessary registration directive Overriding a ...
Error Number: 306 Mizar Message: Attribute symbol expected Description The designated symbol is not declared as category V in the vocabulary: It may be missing ...
Error Number: 203 Mizar Message: Unknown token, maybe the forbidden underscore character used in an identifier Description This error is generated under two conditions ...
Error Number: 138 Mizar Message: Cannot identify a local constant, free in the default type Description The locus being declared depends upon a hidden variable which ...
Error Number: 56 Mizar Message: Disagreement of types Description A local constant being generalized by let disagrees in type with the corresponding quantified ...
Error Number: 55 Mizar Message: Invalid generalization Description A local constant being generalized by let or exemplified by take is deficient with respect ...
Error Number: 129 Mizar Message: Invalid free variables in a Fraenkel operator Description Often happens if the types of variables ("LambdaVariables") parameterizing ...
Error Number: 57 Mizar Message: The type of the instantiated term doesn't widen properly Description The instantiated term is not a sub type of the term's required ...
Error Number: 52 Mizar Message: Invalid assumption Description The assumed condition is not equivalent to the antecedent of the current thesis. Some causes include ...
Error Number: 51 Mizar Message: Invalid conclusion Description Error 51 can result when proving an equivalence (i.e. bi implication, iff) in an unexpected way. Mizar ...
Error Number: 106 Mizar Message: Unknown attribute Description A declared attribute is inapplicable to the subject locus. If the attribute was not a vocabulary symbol ...
Error Number: 251 Mizar Message: "it" is allowed only inside definiens of a public functor or mode Description Predicates and attributes may reference loci (parameter ...
Error Number: 830 Mizar Message: Nothing imported from notations Description A notation directive appears in the environment, but nothing is utilizing any of the ...
Error Number: 834 Mizar Message: Nothing imported from schemes Description A scheme, used to justify a statement, relies on undefined notation. A notations directive ...
Error Number: 20 Mizar Message: The structure of the sentences disagrees with the scheme Description a. A statement Q justified by a scheme does not match the ...
Error Number: 336 Mizar Message: Associative notation must not be used for "iff" and "implies" Description Mizar does not apply a default association rule to consecutive ...
Error Number: 300 Mizar Message: Identifier expected Description Please contribute Typical examples (As far as I know, this is a typical example; I wouldn't call ...
Error Number: 4 Mizar Message: This inference is not accepted Description The checker said "no" Typical examples Please contribute Weird examples I just spent ...
Error Number: 144 Mizar Message: Unknown label Description For MML references often means that you do not have the article in the TheoremDirective. Typical examples ...
Error Number: 143 Mizar Message: No implicit qualification Description Please contribute Typical examples Please contribute Weird examples Can occur when a symbol ...
Error Number: 108 Mizar Message: Invalid list of arguments of redefined constructor Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 937 Mizar Message: Too many arguments Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 735 Mizar Message: Irrelevant variable reservation Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 80 Mizar Message: Cannot be used in a permissive definition Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 731 Mizar Message: The redundant reconsidering of terms Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 69 Mizar Message: Nongeneralizable variable in a definiens Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 807 Mizar Message: Cannot find schemes file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 914 Mizar Message: Too many references in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 803 Mizar Message: Cannot find notations file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 817 Mizar Message: An empty symbol Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 81 Mizar Message: It is meaningful for binary predicates only Description Please contribute Typical examples Please contribute Weird examples Please ...
Number of topics: 40

Related topics: WebHome, BrainstormScratchPad?, FeatureEnhancementRequests?, FeatureToDo?, FeatureUnderConstruction?, FeatureDone?, FeatureNotSuitable?

WebForm
TopicClassification Select one...
ProjectGroup?

ImplementationDate? N/A
Topic revision: r3 - 2002-07-05 - 18:18:00 - WikiRoot
Mizar.ErrorMessage moved from Mizar.ErrorMessages on 2002-07-05 - 09:19 by WikiRoot - put it back
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback