Changeset 2927 for src/common
- Timestamp:
- Mar 21, 2013, 5:17:23 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/ByteValues.ma
r2645 r2927 233 233 completed *) 234 234 | 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) 236 236 | BVnull _ ⇒ OK … false 237 237 | _ ⇒ OK ? true … … 257 257 | _ ⇒ Error ? [MSG NotAnInt32Val] ]. 258 258 259 inductive add_or_sub : Type[0] ≝ 260 | do_add : add_or_sub 261 | do_sub : add_or_sub. 262 263 definition 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 259 269 inductive bebit : Type[0] ≝ 260 270 | BBbit : bool → bebit 261 271 | BBundef : bebit 262 272 | 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. 264 274 265 275 definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
Note: See TracChangeset
for help on using the changeset viewer.