Changeset 2645 for src/common/Errors.ma


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r2500 r2645  
    66include "utilities/monad.ma".
    77include "utilities/option.ma".
     8include "common/ErrorMessages.ma".
    89
    910(* * Error reporting and the error monad. *)
     
    1617
    1718inductive errcode: Type[0] :=
    18   | MSG: String → errcode
    19   | CTX: ∀tag:String. identifier tag → errcode.
     19  | MSG: ErrorMessage → errcode
     20  | CTX: ∀tag:identifierTag. identifier tag → errcode.
    2021
    2122definition errmsg: Type[0] ≝ list errcode.
    2223
    23 definition msg : String → errmsg ≝ λs. [MSG s].
     24definition msg : ErrorMessage → errmsg ≝ λs. [MSG s].
    2425
    2526(* * * The error monad *)
     
    137138
    138139(* A monadic fold_left2 *)
    139 
    140 axiom WrongLength: String.
    141140
    142141let rec mfold_left2
Note: See TracChangeset for help on using the changeset viewer.