Changeset 2927


Ignore:
Timestamp:
Mar 21, 2013, 5:17:23 PM (4 years ago)
Author:
tranquil
Message:

stupid bug in bool_of_beval

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2645 r2927  
    233233                                                   completed *)
    234234  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
    235   | BVByte b ⇒ OK … (eq_bv … (zero …) b)
     235  | BVByte b ⇒ OK … (¬eq_bv … (zero …) b)
    236236  | BVnull _ ⇒  OK … false
    237237  | _ ⇒ OK ? true
     
    257257    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
    258258
     259inductive add_or_sub : Type[0] ≝
     260| do_add : add_or_sub
     261| do_sub : add_or_sub.
     262
     263definition eq_add_or_sub : add_or_sub → add_or_sub → bool ≝
     264λx,y.match x with
     265[ do_add ⇒ match y with [ do_add ⇒ true | _ ⇒ false ]
     266| do_sub ⇒ match y with [ do_sub ⇒ true | _ ⇒ false ]
     267].
     268
    259269inductive bebit : Type[0] ≝
    260270| BBbit : bool → bebit
    261271| BBundef : bebit
    262272| BBptrcarry :
    263   (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
     273  add_or_sub → pointer → ∀p : part.BitVector (8*S p) → bebit.
    264274
    265275definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
Note: See TracChangeset for help on using the changeset viewer.