PC MIZAR, Version 5.2.29
Errors Explanation
Copyright © 1990, 97 Association of Mizar Users
Institute of Mathematics, Bialystok
# 1
It is not true
# 4
This inference is not accepted
# 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
Too many holes
# 21
The structure of sentences disagrees the scheme
# 22
Impossible matching of a locus of a predicate
# 23
Impossible reconstruction of the definiens of a predicate
# 24
Impossible matching of a locus of a functor
# 25
A variable bound in a substituted predicate occurs beyond the predicate
# 26
A variable bound in a substituted functor occurs beyond the functor
# 27
Can't solve cluster ambiguities
# 28
Can't widen the type of the substituted term to the type of functor variable
# 29
Too small number of correspondents of a scheme term
# 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
A 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
# 56
Disagreement of types
# 57
The type of the instatiated term doesn't widen properly
# 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 allowed only inside a proof
# 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
Don't mix cluster correctness with other correctness conditions
# 77
Still not implemented
# 78
It is meaningful for binary predicates only
# 79
Types of arguments must be equal
# 80
Cannot be used in a permissive definition
# 91
Homonimic fields in stucture 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 functor cluster
# 97
Non clusterable attribute
# 100
Inaccessible locus
# 101
Unknown mode
# 102
Unknown predicate
# 103
Unknown functor
# 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 allowed
# 111
Non registered attribute cluster
# 112
Unknown predicate
# 113
Unknown functor
# 114
Unknown mode
# 115
Unknown attribute
# 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
Can't cluser attribute with arguments
# 134
Can't redefine expandable mode
# 135
Inaccessible Selector
# 136
Non registered cluster
# 138
Cannot identify a local constant, free in the default type
# 139
Free variables not allowed in a scheme conclusion
# 140
Unknown variable
# 141
Locus repeated
# 142
Unknown locus
# 143
No implicit qualification
# 144
Unknown label
# 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
# 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
# 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
# 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
# 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
Control characters (e.g. TAB's) are prohibited
# 202
Too large numeral
# 203
Unknown token
# 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
"begin" missing
# 219
Unexpected "proof"
# 229
"redefine" repeated
# 230
Only one "per cases" is allowed in a reasoning
# 231
"per cases" missing
# 232
"case" 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",...,"$8" are allowed only inside definiens of a private constructor
# 251
"it" is allowed only inside definiens of a public functor or mode
# 253
"means" expected
# 271
Redefined mode cannot be expandable
# 272
It's meaningless to redefine cluster
# 274
Don't use means in the 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 theorems file name expected
# 310
Right functor bracket expected
# 311
Paired functor brackets must be of the same kind
# 320
Selector or structure symbol expected
# 321
Predicate symbol or "is" expected
# 329
Selector without argument is allowed only inside a structure pattern
# 330
Unexpected end of an item (perhaps ";" missing)
# 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
# 380
"=" expected
# 381
"if" expected
# 382
"for" expected
# 383
"is" expected
# 384
":" expected
# 385
"->" expected
# 386
"means" expected
# 387
"st" expected
# 388
"as" 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
# 399
Functor pattern expected
# 400
Still not implemented
# 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 justifications
# 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
# 800
Library corrupted
# 801
Cannot find vocabulary file
# 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 clusters file
# 810
A vocabulary symbol 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
Cannot find constructors name on constructor list
# 815
Directive name repeated
# 821
A scheme identifier repeated
# 830
Nothing imported from notations
# 831
Nothing imported from clusters
# 832
Nothing imported from definitions
# 833
Nothing imported from theorems
# 834
Nothing imported from schemes
# 911
Too long term without parentheses
# 912
Too long right nesting of a term
# 913
Too many labels (simultanouesly 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 (simultanouesly 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
# 926
Too many predicate patterns
# 927
Too many functor
# 928
Too many functor patterns
# 929
Too many modes
# 930
Too many mode patterns
# 931
Too many attributes
# 933
Too many structures
# 935
Too many selectors
# 937
Too many registered clusters
# 938
Too many schemes
# 951
Too many imported files
# 999
Too many errors
# 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
# 1255
Ctrl Break
# 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