# Mizar/ErrorCode

< Mizar

ナビゲーションに移動
検索に移動
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 |