include "basics/pts.ma".

inductive ErrorMessage: Type[0] ≝
   MISSING: ErrorMessage
 | EXTERNAL: ErrorMessage
 | AssemblyTooLarge : ErrorMessage
 | Jump_expansion_failed : ErrorMessage
 | ValueIsNotABoolean : ErrorMessage
 | BadCast : ErrorMessage
 | BadlyTypedTerm : ErrorMessage
 | UnknownIdentifier : ErrorMessage
 | BadLvalueTerm : ErrorMessage
 | FailedLoad : ErrorMessage
 | FailedOp : ErrorMessage
 | WrongNumberOfParameters : ErrorMessage
 | FailedStore : ErrorMessage
 | NonsenseState : ErrorMessage
 | ReturnMismatch : ErrorMessage
 | UnknownLabel : ErrorMessage
 | BadFunctionValue : ErrorMessage
 | MainMissing : ErrorMessage
 | UnknownField : ErrorMessage
 | UndeclaredIdentifier : ErrorMessage
 | BadlyTypedAccess : ErrorMessage
 | BadLvalue : ErrorMessage
 | MissingField : ErrorMessage
 | FIXME : ErrorMessage
 | MissingLabel : ErrorMessage
 | ParamGlobalMixup : ErrorMessage
 | DuplicateLabel : ErrorMessage
 | TypeMismatch : ErrorMessage
 | UnknownLocal : ErrorMessage
 | FailedConstant : ErrorMessage
 | BadState : ErrorMessage
 | StoppedMidIO : ErrorMessage
 | UnsupportedOp : ErrorMessage
 | CorruptedPointer: ErrorMessage
 | NotATwoBytesPointer: ErrorMessage
 | ValueNotABoolean: ErrorMessage
 | NotAnInt32Val: ErrorMessage
 | WrongLength: ErrorMessage
 | InitDataStoreFailed : ErrorMessage
 | DuplicateVariable : ErrorMessage
 | MissingId : ErrorMessage
 | IllTypedEvent : ErrorMessage
 | InternalStackFull : ErrorMessage
 | InternalStackEmpty : ErrorMessage
 | BadProgramCounter : ErrorMessage
 | ProgramCounterOutOfCode : ErrorMessage
 | PointNotFound : ErrorMessage
 | LabelNotFound : ErrorMessage
 | MissingSymbol : ErrorMessage
 | BadFunction : ErrorMessage
 | SuccessorNotProvided : ErrorMessage
 | BadPointer : ErrorMessage
 | NoSuccessor : ErrorMessage
 | MissingStackSize : ErrorMessage
 | ExternalMain: ErrorMessage
 | BadRegister : ErrorMessage
 | BadMain : ErrorMessage
 | MissingRegister : ErrorMessage
 | MissingStatement : ErrorMessage
 | BadJumpTable : ErrorMessage
 | BadJumpValue : ErrorMessage
 | FinalState : ErrorMessage
 | EmptyStack: ErrorMessage
 | OutOfBounds: ErrorMessage
 | UnexpectedIO : ErrorMessage
 | TerminatedEarly : ErrorMessage
 | BadCostLabelling : ErrorMessage
 | RepeatedCostLabel : ErrorMessage
 | NotTerminated : ErrorMessage
 | RepeatedCostLabel : ErrorMessage
 | FramesEmptyOnPop : ErrorMessage
 | BlockInFramesCorrupted : ErrorMessage
 | FrameErrorOnPush : ErrorMessage
 | FrameErrorOnPop : ErrorMessage
 | FunctionNotFound : ErrorMessage
 | StackOverflow : ErrorMessage.