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/PreIdentifiers.ma

    r1515 r2645  
    66
    77include "basics/types.ma".
    8 include "ASM/String.ma".
    98include "utilities/binary/positive.ma".
    109
     
    1211   provide extra type checking. *)
    1312
    14 inductive identifier (tag:String) : Type[0] ≝
     13inductive identifierTag: Type[0] ≝
     14   Label : identifierTag
     15 | CostTag : identifierTag
     16 | RegisterTag : identifierTag
     17 | LabelTag : identifierTag
     18 | SymbolTag : identifierTag.
     19
     20inductive identifier (tag:identifierTag) : Type[0] ≝
    1521  an_identifier : Pos → identifier tag.
Note: See TracChangeset for help on using the changeset viewer.