Skip to topic | Skip to bottom
Home
Mizar

edit

Mizar.ErrorMessager1.3 - 05 Jul 2002 - 18:18 - WikiRoottopic end
Start of topic | Skip to actions

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
ErrorNo300
JesseAlama
25 Jan 2007 - 02:13 - r1.2

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
08 Aug 2002 - 21:23 - r1.2

Error Number: 4 Mizar Message: This inference is not accepted Description The checker said "no" Typical examples Please contribute Weird examples I just spent 5 minutes ...
ErrorNo144
JosefUrban
08 Aug 2002 - 20:40 - r1.2

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 ...
ErrorNo165
JosefUrban
08 Aug 2002 - 20:21 - r1.2

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. Typical ...
ErrorNo143
JosefUrban
06 Aug 2002 - 14:40 - r1.2

Error Number: 143 Mizar Message: No implicit qualification Description Please contribute Typical examples Please contribute Weird examples Can occur when a symbol ...
ErrorNo129
JosefUrban
25 Jul 2002 - 17:45 - r1.2

Error Number: 129 Mizar Message: Invalid free variables in a Fraenkel operator Description Often happens if the types of variables ("LambdaVariables") parametrizing ...
ErrorNo108
JosefUrban
23 Jul 2002 - 10:37 - r1.2

Error Number: 108 Mizar Message: Invalid list of arguments of redefined constructor Description Please contribute Typical examples Please contribute Weird examples ...
ErrorNo62
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 62 Mizar Message: Free variables not allowed in an iterative equality Description Please contribute Typical examples Please contribute Weird examples ...
ErrorNo63
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 63 Mizar Message: Unexpected proof Description Please contribute Typical examples Please contribute Weird examples Please contribute
ErrorNo64
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 64 Mizar Message: Invalid exemplification in a diffuse statement Description Please contribute Typical examples Please contribute Weird examples Please ...
ErrorNo65
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 65 Mizar Message: "thesis" is allowed only inside a proof Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo68
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 68 Mizar Message: Nongeneralizable variable in the skeleton of a reasoning Description Please contribute Typical examples Please contribute Weird examples ...
ErrorNo69
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 69 Mizar Message: Nongeneralizable variable in a definiens Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo70
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 70 Mizar Message: Something remains to be proved Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo703
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 703 Mizar Message: Unnecessary "proof thus thesis; end;" Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo704
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 704 Mizar Message: Irrelevant signature directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo706
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 706 Mizar Message: Unnecessary theorems directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo707
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 707 Mizar Message: Unnecessary schemes directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo708
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 708 Mizar Message: Theorem should be replaced by an equal one Description Please contribute Typical examples Please contribute Weird examples Please ...
ErrorNo709
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 709 Mizar Message: Irrelevant vocabulary directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo710
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 710 Mizar Message: Irrelevant definitions directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo711
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 711 Mizar Message: Identity functor definition Description Please contribute Typical examples Please contribute Weird examples Please contribute
ErrorNo712
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 712 Mizar Message: Synonym of a functor definition Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo713
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 713 Mizar Message: Irrelevant redefinition of a functor Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo714
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 714 Mizar Message: Irrelevant redefinition of a mode Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo715
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 715 Mizar Message: Irrelevant reconsider of a variable Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo716
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 716 Mizar Message: Irrelevant reconsider of a term Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo717
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 717 Mizar Message: Irrelevant reconsider Description Please contribute Typical examples Please contribute Weird examples Please contribute
ErrorNo72
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 72 Mizar Message: Unexpected correctness condition Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo720
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 720 Mizar Message: The first two arguments of the iterative equality are equal Description Please contribute Typical examples Please contribute Weird ...
ErrorNo721
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 721 Mizar Message: The first argument of the iterative equality is equal with a next one Description Please contribute Typical examples Please contribute ...
ErrorNo722
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 722 Mizar Message: The second argument of the iterative equality is equal with a next one Description Please contribute Typical examples Please contribute ...
ErrorNo724
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 724 Mizar Message: This argument of the iterative equality is equal with a next one Description Please contribute Typical examples Please contribute ...
ErrorNo725
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 725 Mizar Message: The equal argument of the iterative equality with a previous one Description Please contribute Typical examples Please contribute ...
ErrorNo73
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 73 Mizar Message: Correctness condition missing Description Please contribute Typical examples Please contribute Weird examples Please contribute
ErrorNo730
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 730 Mizar Message: The redundant reconsidering of variables Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo731
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 731 Mizar Message: The redundant reconsidering of terms Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo732
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 732 Mizar Message: The redundant reconsidering of a variable Description Please contribute Typical examples Please contribute Weird examples Please ...
ErrorNo733
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 733 Mizar Message: The redundant reconsidering of a term Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
ErrorNo734
WikiRoot
05 Jul 2002 - 10:20 - NEW

Error Number: 734 Mizar Message: The redundant considering Description Please contribute Typical examples Please contribute Weird examples Please contribute
Number of topics: 40

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


to top

End of topic
Skip to action links | Back to top

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


Edit | Attach image or document | Printable version | Raw text | More topic actions
Revisions: | r1.3 | > | r1.2 | > | r1.1 | Total page history | Backlinks
Mizar.ErrorMessage moved from Mizar.ErrorMessages on 05 Jul 2002 - 09:19 by WikiRoot - put it back
You are here: Mizar > ErrorMessage

to top

Copyright © 1999-2008 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding Mizar TWiki? Send feedback