ErrorMessage < Mizar

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ErrorNo937

NEW - 2002-07-05 - 10:20

Error Number: 937 Mizar Message: Too many arguments Description Please contribute Typical examples Please contribute Weird examples Please contribute

ErrorNo735

NEW - 2002-07-05 - 10:20

Error Number: 735 Mizar Message: Irrelevant variable reservation Description Please contribute Typical examples Please contribute Weird examples Please contribute ...

ErrorNo80

NEW - 2002-07-05 - 10:20

Error Number: 80 Mizar Message: Cannot be used in a permissive definition Description Please contribute Typical examples Please contribute Weird examples Please ...

ErrorNo731

NEW - 2002-07-05 - 10:20

Error Number: 731 Mizar Message: The redundant reconsidering of terms Description Please contribute Typical examples Please contribute Weird examples Please contribute ...

ErrorNo69

NEW - 2002-07-05 - 10:20

Error Number: 69 Mizar Message: Nongeneralizable variable in a definiens Description Please contribute Typical examples Please contribute Weird examples Please ...

ErrorNo807

NEW - 2002-07-05 - 10:20

Error Number: 807 Mizar Message: Cannot find schemes file Description Please contribute Typical examples Please contribute Weird examples Please contribute

ErrorNo914

NEW - 2002-07-05 - 10:20

Error Number: 914 Mizar Message: Too many references in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...

ErrorNo803

NEW - 2002-07-05 - 10:20

Error Number: 803 Mizar Message: Cannot find notations file Description Please contribute Typical examples Please contribute Weird examples Please contribute

ErrorNo817

NEW - 2002-07-05 - 10:20

Error Number: 817 Mizar Message: An empty symbol Description Please contribute Typical examples Please contribute Weird examples Please contribute

ErrorNo81

NEW - 2002-07-05 - 10:20

Error Number: 81 Mizar Message: It is meaningful for binary predicates only Description Please contribute Typical examples Please contribute Weird examples Please ...

ErrorNo933