Changeset 2443 for src/common/ByteValues.ma
- Timestamp:
- Nov 8, 2012, 2:27:54 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/ByteValues.ma
r2435 r2443 103 103 axiom NotATwoBytesPointer: String. 104 104 105 (* Fails if the address is not representable as a pair *) 106 definition beval_pair_of_pointer: pointer → res (beval × beval) ≝ 107 λp. OK … (list_to_pair … (bevals_of_pointer p) (refl …)). 105 (* Should fail if the address is not representable as a pair 106 As we only have 16 bit addresses atm, it never fails *) 107 definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝ 108 λp.list_to_pair … (bevals_of_pointer p) (refl …). 108 109 (* 109 110 λp. match p with [ mk_pointer pty pbl pok poff ⇒
Note: See TracChangeset
for help on using the changeset viewer.