| 1 | include "basics/pts.ma". |
|---|
| 2 | |
|---|
| 3 | inductive ErrorMessage: Type[0] ≝ |
|---|
| 4 | MISSING: ErrorMessage |
|---|
| 5 | | EXTERNAL: ErrorMessage |
|---|
| 6 | | Jump_expansion_failed : ErrorMessage |
|---|
| 7 | | ValueIsNotABoolean : ErrorMessage |
|---|
| 8 | | BadCast : ErrorMessage |
|---|
| 9 | | BadlyTypedTerm : ErrorMessage |
|---|
| 10 | | UnknownIdentifier : ErrorMessage |
|---|
| 11 | | BadLvalueTerm : ErrorMessage |
|---|
| 12 | | FailedLoad : ErrorMessage |
|---|
| 13 | | FailedOp : ErrorMessage |
|---|
| 14 | | WrongNumberOfParameters : ErrorMessage |
|---|
| 15 | | FailedStore : ErrorMessage |
|---|
| 16 | | NonsenseState : ErrorMessage |
|---|
| 17 | | ReturnMismatch : ErrorMessage |
|---|
| 18 | | UnknownLabel : ErrorMessage |
|---|
| 19 | | BadFunctionValue : ErrorMessage |
|---|
| 20 | | MainMissing : ErrorMessage |
|---|
| 21 | | UnknownField : ErrorMessage |
|---|
| 22 | | UndeclaredIdentifier : ErrorMessage |
|---|
| 23 | | BadlyTypedAccess : ErrorMessage |
|---|
| 24 | | BadLvalue : ErrorMessage |
|---|
| 25 | | MissingField : ErrorMessage |
|---|
| 26 | | FIXME : ErrorMessage |
|---|
| 27 | | MissingLabel : ErrorMessage |
|---|
| 28 | | ParamGlobalMixup : ErrorMessage |
|---|
| 29 | | DuplicateLabel : ErrorMessage |
|---|
| 30 | | TypeMismatch : ErrorMessage |
|---|
| 31 | | UnknownLocal : ErrorMessage |
|---|
| 32 | | FailedConstant : ErrorMessage |
|---|
| 33 | | BadState : ErrorMessage |
|---|
| 34 | | StoppedMidIO : ErrorMessage |
|---|
| 35 | | UnsupportedOp : ErrorMessage |
|---|
| 36 | | CorruptedPointer: ErrorMessage |
|---|
| 37 | | NotATwoBytesPointer: ErrorMessage |
|---|
| 38 | | ValueNotABoolean: ErrorMessage |
|---|
| 39 | | NotAnInt32Val: ErrorMessage |
|---|
| 40 | | WrongLength: ErrorMessage |
|---|
| 41 | | InitDataStoreFailed : ErrorMessage |
|---|
| 42 | | DuplicateVariable : ErrorMessage |
|---|
| 43 | | MissingId : ErrorMessage |
|---|
| 44 | | IllTypedEvent : ErrorMessage |
|---|
| 45 | | InternalStackFull : ErrorMessage |
|---|
| 46 | | InternalStackEmpty : ErrorMessage |
|---|
| 47 | | BadProgramCounter : ErrorMessage |
|---|
| 48 | | ProgramCounterOutOfCode : ErrorMessage |
|---|
| 49 | | PointNotFound : ErrorMessage |
|---|
| 50 | | LabelNotFound : ErrorMessage |
|---|
| 51 | | MissingSymbol : ErrorMessage |
|---|
| 52 | | BadFunction : ErrorMessage |
|---|
| 53 | | SuccessorNotProvided : ErrorMessage |
|---|
| 54 | | BadPointer : ErrorMessage |
|---|
| 55 | | NoSuccessor : ErrorMessage |
|---|
| 56 | | MissingStackSize : ErrorMessage |
|---|
| 57 | | ExternalMain: ErrorMessage |
|---|
| 58 | | BadRegister : ErrorMessage |
|---|
| 59 | | BadMain : ErrorMessage |
|---|
| 60 | | MissingRegister : ErrorMessage |
|---|
| 61 | | MissingStatement : ErrorMessage |
|---|
| 62 | | BadJumpTable : ErrorMessage |
|---|
| 63 | | BadJumpValue : ErrorMessage |
|---|
| 64 | | FinalState : ErrorMessage |
|---|
| 65 | | EmptyStack: ErrorMessage |
|---|
| 66 | | OutOfBounds: ErrorMessage. |
|---|
