コンテンツにスキップ

Mizar/ErrorCode

出典: フリー教科書『ウィキブックス(Wikibooks)』
code 意味 日本語意味 environ 対応方法
1 It is not true
4 This inference is not accepted この推論は不正確 registrations 正確な定義、定理を by 以後に記す
8 Too many instantiations
9 Too many instantiations
10 Too many basic sentences in an inference
11 Too many constants in an inference
12 Too long universal prefix
13 Too many complexes
14 Too many terms in an inference
15 Too many equalities in an inference
16 Collection overflow
20 The structure of the sentences disagrees with the scheme
21 Invalid instantiation of a scheme functor
22 Invalid instantiation of a scheme predicate
23 Invalid order of arguments in the instantiated predicate
24 Instantiations of the same scheme predicate do not match
25 Instantiations of the same scheme constant do not match
26 Substituted constant does not expand properly
27 Invalid instantiation of a scheme constant
28 Invalid list of arguments of a functor
29 Instantiations of the same scheme functor do not match
30 Invalid type of the instantiated functor
31 Disagreement of correspondents of a constant
32 Too many fillings of a functor
33 Too many fillings of a predicate
40 Non-unique matching of a locus of the substitute of a predicate variable
41 Non-unique matching of a locus of the substitute of a functor variable
42 Non-unique matching of a locus of the substitute of a functor variable
43 Cannot decompose a conjunction of formal sentences
44 Formal predicate in a Fraenkel operator of formal construction
45 Wrong order of the declarations of scheme functor or nested functor
46 Probably the incorporation of an argument
50 Nongeneralizable variable in the skeleton of a reasoning
51 Invalid conclusion 無効な結論 述語定義が一致しない。型形式で定義したものと、この式で使われている型が一致しない
52 Invalid assumption
53 Invalid case
54 The cases are not exhausted
55 Invalid generalization 無効な一般化 スケルトンの証明に無関係な任意変数をもってきたのでerrorが出た
56 Disagreement of types
57 The type of the instatiated term doesn't widen properly
58 Mixing "case" with "suppose" is not allowed in one "per cases" reasoning
59 The theses in each case should be equal formulae
60 Something remains to be proved in this case
62 Free variables not allowed in an iterative equality
63 Unexpected proof
64 Invalid exemplification in a diffuse statement
65 "thesis" is only allowed inside a proof
66 "axiom" is only allowed in an axiomatic file
68 Nongeneralizable variable in the skeleton of a reasoning
69 Nongeneralizable variable in a definiens
70 Something remains to be proved まだ証明されていません
72 Unexpected correctness condition
73 Correctness condition missing
76 Registration correctness condition mismatch
77 Still not implemented
78 The type of the argument must widen to the result type
79 Types of arguments must be equal
80 Cannot be used in a permissive definition
81 It is only meaningful for binary predicates
82 It is only meaningful for binary functors
83 It is only meaningful for unary functors
84 The result type is not invariant under swapping the arguments
85 The result type must widen to the type of the argument
89 As yet not implemented for redefined functors
90 Attributes are not allowed in a prefix
91 Homonymic fields in structure declaration
92 Type of the field must be equal to the type in prefix
93 Missing field of a prefix
94 Prefix must be a structure
95 Inconsistent cluster
96 Only standard functors and selectors can be used in a functorial cluster registration
97 Non clusterable attribute
98 Cannot mix left and right pattern arguments
99 The argument(s) must belong to the left or right pattern
100 Unused locus
101 Unknown mode
102 Unknown predicate
103 Unknown functor functorが未定義 constructors 演算を認知しない。演算子の左か右の型(mode)が演算子で使われる型と一致していない
104 Unknown structure
105 Illegal projection
106 Unknown attribute
107 Invalid list of arguments of redefined constructor
108 Invalid list of arguments of redefined constructor
109 Invalid order of arguments of redefined constructor
110 Only nullary prefixes are allowed
111 Non registered attribute cluster
112 Unknown predicate
113 Unknown functor
114 Unknown mode
115 Unknown attribute 属性が未定義 notations cluster requirements に型ファイル名を追加する必要があります
116 Invalid "qua"
117 Invalid specification
118 Invalid specification
119 Illegal cluster
120 Disagreement of argument types
121 Disagreement of argument types
122 Disagreement of argument types
123 Disagreement of argument types
124 Disagreement of argument types
125 Argument of a selector must be a structure
126 Unknown selector functor
127 Argument must be an elementary type
128 Arguments must be elementary types
129 Invalid free variables in a Fraenkel operator
130 Redefinition of an attribute with predicate pattern is not allowed
131 No reserved type for a variable, free in the default type 未登録の変数タイプ、ディフォルトは形無しタイプ
132 Invalid "exactly"
133 Cannot cluster attribute with arguments
134 Cannot redefine expandable mode
135 Inaccessible selector
136 Non registered cluster 無登録なクラスタ registrations registrations にファイル名を追加しなければならない
137 "SUBSET" missing in the "requirements" directive
138 Cannot identify a local constant, free in the default type
139 Invalid type of an argument.
140 Unknown variable
141 Locus repeated
142 Unknown locus 場所が未定義
143 No implicit qualification
144 Unknown label ラベルが未定義 theorems
145 Inaccessible label
146 Theorem number must be greater than 0
147 Unknown theorems file
148 Unknown private functor 個人的関数が未定義
149 Unknown private predicate
150 A variable free in default type has explicit qualification
151 Unknown mode format モードが未定義
152 Unknown functor format 関数が未定義
153 Unknown predicate format predicateが未定義
154 Unknown field
155 Unknown prefix
156 Invalid equality format
157 Exactly one term is expected before "is"
158 Two different formats for a structure symbol
159 Invalid iterative equality
160 This variable still cannot be accessed
161 Fixed variables cannot be postqualified
162 A free variable identified with a new implicit qualification
163 Disagreement of reservations of a free variable
164 Nothing to link リンク先が無い
165 Unknown functor format 関数形式が未定義 notations
166 Unknown functor format
167 Unknown functor format
168 Unknown functor format
169 Unknown functor format
170 Unknown functor format
171 Unknown functor format
172 Unknown functor format
173 Unknown functor format
174 Unknown functor format
175 Unknown attribute format 定義されていない属性 notations notationsに用語・使用法・形式ファイル名を記述しなければならない
176 Unknown structure format
177 Link assumes a straightforward justification
178 Link assumes a straightforward justification
179 It is not a locus
180 Too many arguments
181 Not so many arguments in this definition
182 Unknown selector format
183 Accessible mode format has empty list of arguments
184 Accessible structure format has empty list of arguments
185 Unknown structured mode format
186 "equals" is only allowed for functors
189 Left and right pattern must have the same number of arguments
190 Inaccessible theorem constructors constr -f text/hoge.miz ラベル名 で必要なconstroutorsを調べて追加
191 Unknown scheme
192 Inaccessible theorem
193 Inaccessible scheme
194 Wrong number of premises
195 Scheme uses constructors which are not in your environment
196 Unknown scheme
197 Scheme definition repeated
198 It is meaningless to define an antonym to a functor or a mode
199 Inaccessible definitional theorem
200 Too long source line
201 Only characters with decimal ASCII codes between 32 and 126 are allowed
202 Too large numeral
203 Unknown token, maybe an illegal character used in an identifier
203 Unknown token, maybe the forbidden underscore character used in an identifier 未定義のトークン、おそらく識別子に禁じられた隠文字を使っている theorems
210 Wrong item in environment declaration
211 Unexpected "environ"
212 "environ" expected
213 "begin" missing "始め"がない
214 "end" missing "終り"がない
215 No pairing "end" for this word
216 Unexpected "end"
217 ";" missing
218 Unexpected "(" - parenthesizing attributes is not allowed
219 Unexpected "proof"
220 Local predicates are not allowed in library items
221 Local functors are not allowed in library items
222 Local constants are not allowed in library items
223 Adjective cluster expected
228 Unexpected "reconsider"
229 "redefine" repeated
230 Only one "per cases" is allowed in a reasoning
231 "per cases" missing
232 "case" or "suppose" expected
240 Definition blocks must not be nested
241 Directives are not allowed in the text proper
242 "reserve", "struct", "scheme" and "theorem" not allowed in a definition block
250 "$1",...,"$10" are only allowed inside the definiens of a private constructor
251 "it" is only allowed inside the definiens of a public functor or mode
253 "means" or "equals" expected
255 It is not allowed for expandable modes
256 "of" expected
257 Right term must be a subterm of the left term
258 Choice and Fraenkel terms are not allowed in reductions
271 Redefined mode cannot be expandable
272 It is meaningless to redefine a cluster
273 "redefine" is not allowed here
274 "means" not allowed in a definition of an expandable mode
300 Identifier expected 識別子が不明
301 Predicate symbol expected
302 Functor symbol expected 関数記号が不明
303 Mode symbol expected
304 Structure symbol expected
305 Selector symbol expected
306 Attribute symbol expected 属性記号が不明
307 Numeral expected
308 Identifier or theorem file name expected
309 Mode symbol or attribute symbol expected モード記号、または、属性記号が不明
310 Right functor bracket expected 右の関数括弧が不明
311 Paired functor brackets must be of the same kind
312 Scheme reference is not allowed in a simple justification
313 "sch" expected
314 Incorrect beginning of a pattern
315 Mode "set" cannot be parametrized
320 Selector or structure symbol expected
321 Predicate symbol or "is" expected つづりが不明。 vocabularies vocabulariesに用語ファイル名を記述しなければならない
329 Selector without arguments is only allowed inside a structure pattern
330 Unexpected end of an items(perhaps ";" missing) そんなラベルは知らない(どこにあるの?) theorems 「;」の書き忘れ、もしくは定義定理のラベルの場合はtheoremsにライブラリを追加します
336 Associative notation must not be used for "iff" and "implies"
340 "holds", "for" or "ex" expected
350 "that" expected
351 "cases" expected
360 "(" expected
361 "[" expected
362 "{" expected
363 "(#" expected
364 "(" or "[" expected
370 ")" expected
371 "]" expected
372 "}" expected
373 "#)" expected
374 Incorrect order of arguments in an attribute definition
375 Wrong beginning of a cluster registration
376 Incorrect functorial registration - addjectives expected
377 Incorrect conditional registration - type expected
378 Parenthesizing adjective clusters is not allowed
379 Term list is not allowed here
380 "=" expected
381 "if" expected
382 "for" expected
383 "is" expected
384 ":" expected
385 "->" expected
386 "means" or "equals" expected
387 "st" expected
388 "as" expected
389 "proof" expected
390 "and" expected
391 Incorrect beginning of a text item テキストアイテムの始まりが間違っています
392 Incorrect beginning of a definition item
393 Incorrect beginning of a reasoning item
394 Statement expected
395 Justification expected
396 Formula expected
397 Term expected
398 Type expected タイプが定義されていない。 vocabularies vocabulariesに用語ファイルを記述しなければならない
399 Functor pattern expected
400 Still not implemented
401 "not" expected
402 A bare infinitive expected
403 "such" expected
404 "to" expected
405 "for" expected
406 "for" or "->" expected
450 Too many variables
451 Too many predicate formats
452 Too many functor formats
453 Too many mode formats
454 Too large theorem number
455 Too many labels in a definition block
456 Too many references in an inference
458 Too many private predicates
459 Too many private functors
460 Too many reserved identifiers
461 Too many free variables
462 Too many modes
465 Too many predicates
466 Too many functors
467 Too many structures
468 Too many selectors
469 Too many loci
470 Too complicated term
471 Too many selectors in one structure definition
472 Too many references
473 Too many premisses in a simple justification
474 Too complicated term
476 Too many default signature files
477 Too many predicate, mode or functor symbols
478 Too many labels
479 Too many loci in one definition block
480 Too many default vocabulary files
481 Too many functor symbols in default vocabulary files
482 Too many free variable scopes
483 Too many variables
484 Too many reservations
485 Too nested reasoning
486 Too many functor formats
487 Too many scheme identifiers
488 Too many unreserved free variables
489 Memory handling in unifier failed
490 Too many free variables in reservations
491 Too many structure formats
492 Too many functor formats
493 Too many parameters in one scheme
494 Too complicated scheme (too many external variables)
495 Too complicated scheme (too many occurrences of a functor variable)
496 Too complicated scheme (too many occurrences of a predicate variable)
497 Too many functor symbols
498 Too many occurrences of arguments of a second order variable
499 Too many errors
601 Irrelevant label
602 Irrelevant reference
603 Irrelevant linking
604 Irrelevant inference
605 Irrelevant linked inference
607 Justification can be straightforward
608 Linkable statement
609 Irrelevant "that"
610 Beginning of an inaccessible item
611 End of an inaccessible item
612 Beginning of inaccessible conditions
613 End of inaccessible conditions
614 Duplicated label identifier
615 Unexpected "@proof"
616 "be" recommended
703 Unnecessary "proof thus thesis; end;"
704 Irrelevant signature directive
706 Unnecessary item in the "theorems" directive
707 Unnecessary item in the "schemes" directive
708 Theorem should be replaced by an equal one
709 Irrelevant item in the "vocabularies" directive
710 Irrelevant item in the "definitions" directive
711 Identity functor definition
712 Synonym of a functor definition
713 Irrelevant redefinition of a functor
714 Irrelevant redefinition of a mode
715 Irrelevant "reconsider" of a variable
716 Irrelevant "reconsider" of a term
717 Irrelevant reconsider
720 The first two arguments of the iterative equality are equal
721 The first argument of the iterative equality is equal to the next one
722 The second argument of the iterative equality is equal to the next one
724 This argument of the iterative equality is equal to the next one
725 This argument of the iterative equality is equal to the previous one
730 Redundant reconsidering of variables
731 Redundant reconsidering of terms
732 Redundant reconsidering of a variable
733 Redundant reconsidering of a term
734 Redundant considering
735 Irrelevant variable reservation
736 Unused private functor
737 Unused private predicate
738 Unused variable introduced by "set"
739 The variable introduced by "set" used only once
740 Unused variable introduced by "given"
742 Unused variable introduced by "take"
743 Unused variable introduced by "consider"
746 References can be moved to the next step of this iterative equality
800 Library corrupted
801 Cannot find vocabulary file 用語ファイルが見つからない vocabularies vocabulariesに正しい用語ファイル名を記述しなければならない
802 Cannot find formats file
803 Cannot find notations file
804 Cannot find signature file
805 Cannot find definitions file
806 Cannot find theorems file
807 Cannot find schemes file
808 Cannot find constructors file
809 Cannot find registrations file
810 Directive name repeated
811 Invalid priority of a functor symbol on a vocabulary file
812 An empty line on a vocabulary file
813 Invalid qualifier on a vocabulary file
814 Invalid character or space in a symbol
815 A vocabulary symbol repeated
816 Invalid priority
817 An empty symbol
821 A scheme identifier repeated
825 Cannot find constructors name on constructor list
830 Nothing imported from notations notations の設定が不十分! constractors constractorsにもファイル名を追加!(大抵、notationsと同じ名前)
831 Nothing imported from registrations
832 Nothing imported from definitions
833 Nothing imported from theorems
834 Nothing imported from schemes
855 Cannot find requirements file
856 Inaccessible requirements directive
891 MML identifier should be written in capitals
892 MML identifier should be at most eight characters long
900 Too complex skeleton
911 Too long term without parentheses
912 Too long right nesting of a term
913 Too many labels (simultaneously accessible)
914 Too many references in an inference
915 Too many ranges of free variables
916 Too many reservations
917 Too many free variables in reservations
918 Too many variables (simultaneously accessible)
919 Too many reserved identifiers
920 Too many private functors
921 Too many private predicates
923 Too many different clusters
924 Common number of loci exceeded
925 Too many predicate patterns
926 Too many functors
927 Too many functor patterns
928 Too many modes
929 Too many mode patterns
930 Too many attributes
931 Too many attribute patterns
933 Too many structures
935 Too many selectors
936 Too many registered clusters
937 Too many arguments
938 Too many terms
950 Too many schemes
951 Too many imported files
No.1000 Turbo Pascal Errors ( ErrNr = PascalErrNr+1000 )
1001 Invalid function number
1002 File not found
1003 Path not found
1004 Too many open files
1005 File access denied
1006 Invalid file handle
1012 Invalid file access code
1015 Invalid drive number
1016 Cannot remove current directory
1017 Cannot rename across drives
1018 No more files
1100 Disk read error
1101 Disk write error
1102 File not assigned
1103 File not open
1104 File not open for input
1105 File not open for output
1106 Invalid numeric format
1150 Disk is write-protected
1151 Bad drive request struct length
1152 Drive not ready
1154 CRC error in data
1156 Disk seek error
1157 Unknown media type
1158 Sector Not Found
1159 Printer out of paper
1160 Device write fault
1161 Device read fault
1162 Hardware failure
1200 Division by zero
1201 Range check error
1202 Stack overflow error
1203 Heap overflow error
1204 Invalid pointer operation
1205 Floating point overflow
1206 Floating point underflow
1207 Invalid floating point operation
1208 Overlay manager not installed
1209 Overlay file read error
1210 Object not initialized
1211 Call to abstract method
1212 Stream registration error
1213 Collection index out of range
1214 Collection overflow error
1215 Arithmetic overflow error
1216 General Protection fault
1217 Segmentation fault
1255 Ctrl Break
No.1990 I/O stream error:
1994 I/O stream error: Put of unregistered object type
1995 I/O stream error: Get of unregistered object type
1996 I/O stream error: Cannot expand stream
1997 I/O stream error: Read beyond end of stream
1998 I/O stream error: Cannot initialize stream
1999 I/O stream error: Access error