Changeset 1873 for src/common/AST.ma


Ignore:
Timestamp:
Apr 4, 2012, 6:48:24 PM (9 years ago)
Author:
campbell
Message:

Fix up earlier front-end value conversion work.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1872 r1873  
    130130   (At the time of writing this is only used for bitsize_of_intsize.) *)
    131131
     132definition pred_size_intsize : intsize → nat ≝
     133λsz. match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     134
    132135definition size_intsize : intsize → nat ≝
    133 λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     136λsz. S (pred_size_intsize sz).
    134137
    135138definition bitsize_of_intsize : intsize → nat ≝
    136 λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
     139λsz. size_intsize sz * 8.
    137140
    138141definition eq_intsize : intsize → intsize → bool ≝
Note: See TracChangeset for help on using the changeset viewer.