Changeset 2645 for src/joint/Joint.ma


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (8 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/joint/Joint.ma

    r2595 r2645  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "joint/String.ma".
    910
    1011(* Here is the structure of parameter records (downward edges are coercions,
     
    108109  | extension_seq : ext_seq p → joint_seq p globals.
    109110
    110 axiom EmptyString : String.
    111111definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
    112112
Note: See TracChangeset for help on using the changeset viewer.