AllErrorMessages < Mizar

TWiki>

Mizar Web>ErrorMessage>AllErrorMessages (2002-07-05, WikiRoot)EditAttach

Description of The Mizar Error Messages

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

Results from Mizar web retrieved at 18:45 (GMT)

ErrorNo9

BorisSchminke

r2 - 2011-10-05 - 13:51

Error Number: 9 Mizar Message: Too many instantiations Description Please contribute Typical examples environ vocabularies ZFMISC 1, PRE TOPC, EUCLID; constructors ...

ErrorNo93

BorisSchminke

r2 - 2010-08-26 - 12:19

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

ErrorNo856

BorisSchminke

r3 - 2010-08-17 - 17:41

Error Number: 856 Mizar Message: Inaccessible requirements directive Description A requirements directive needs prerequisite information that is not being supplied ...

ErrorNo103

GregFrascadore

r3 - 2009-11-29 - 15:47

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

ErrorNo165

GregFrascadore

r3 - 2009-10-20 - 22:32

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

ErrorNo166

GregFrascadore

r2 - 2009-10-20 - 22:25

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

ErrorNo148

GregFrascadore

r3 - 2009-10-20 - 21:55

Error Number: 148 Mizar Message: Unknown private functor Description This can be caused by referencing a function without importing the necessary vocabulary. Importing ...

ErrorNo397

GregFrascadore

r2 - 2009-10-20 - 21:53

Error Number: 397 Mizar Message: Term expected Description An off category or unknown symbol appears where a term is expected. Some possible causes include: ...

ErrorNo102

GregFrascadore

r3 - 2009-10-18 - 04:23

Error Number: 102 Mizar Message: Unknown predicate Description Some causes of this error are: Omitting a necessary registration directive Overriding a ...

ErrorNo306

GregFrascadore

r2 - 2009-07-26 - 20:50

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

ErrorNo203

GregFrascadore

r2 - 2009-07-21 - 01:26

Error Number: 203 Mizar Message: Unknown token, maybe the forbidden underscore character used in an identifier Description This error is generated under two conditions ...

ErrorNo138

GregFrascadore

r2 - 2009-07-18 - 15:40

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

ErrorNo56

GregFrascadore

r2 - 2009-06-03 - 14:17

Error Number: 56 Mizar Message: Disagreement of types Description A local constant being generalized by let disagrees in type with the corresponding quantified ...

ErrorNo55

GregFrascadore

r3 - 2009-06-03 - 12:58

Error Number: 55 Mizar Message: Invalid generalization Description A local constant being generalized by let or exemplified by take is deficient with respect ...

ErrorNo129

GregFrascadore

r3 - 2009-05-24 - 14:46

Error Number: 129 Mizar Message: Invalid free variables in a Fraenkel operator Description Often happens if the types of variables ("LambdaVariables") parameterizing ...

ErrorNo57

GregFrascadore

r2 - 2009-05-22 - 03:05

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

ErrorNo52

GregFrascadore

r2 - 2009-05-16 - 14:31

Error Number: 52 Mizar Message: Invalid assumption Description The assumed condition is not equivalent to the antecedent of the current thesis. Some causes include ...

ErrorNo51

GregFrascadore

r2 - 2009-05-08 - 23:05

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

ErrorNo106

GregFrascadore

r3 - 2009-04-20 - 13:17

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

ErrorNo251

GregFrascadore

r2 - 2009-04-20 - 02:42

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

ErrorNo830

GregFrascadore

r3 - 2009-04-14 - 16:50

Error Number: 830 Mizar Message: Nothing imported from notations Description A notation directive appears in the environment, but nothing is utilizing any of the ...

ErrorNo834

GregFrascadore

r2 - 2009-04-04 - 05:09

Error Number: 834 Mizar Message: Nothing imported from schemes Description A scheme, used to justify a statement, relies on undefined notation. A notations directive ...

ErrorNo20

GregFrascadore

r3 - 2009-03-31 - 04:44

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

ErrorNo336

GregFrascadore

r3 - 2009-03-31 - 02:52

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

ErrorNo300

JesseAlama

r2 - 2007-01-25 - 02:13

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

ErrorNo4

JosefUrban

r2 - 2002-08-08 - 21:23

Error Number: 4 Mizar Message: This inference is not accepted Description The checker said "no" Typical examples Please contribute Weird examples I just spent ...

ErrorNo144

JosefUrban

r2 - 2002-08-08 - 20:40

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

ErrorNo143

JosefUrban

r2 - 2002-08-06 - 14:40

Error Number: 143 Mizar Message: No implicit qualification Description Please contribute Typical examples Please contribute Weird examples Can occur when a symbol ...

ErrorNo108

JosefUrban

r2 - 2002-07-23 - 10:37

Error Number: 108 Mizar Message: Invalid list of arguments of redefined constructor Description Please contribute Typical examples Please contribute Weird examples ...

WebForm
TopicClassification	Select one...
ProjectGroup?
ImplementationDate?	N/A