Changeset 2443 for src/common/ByteValues.ma

Timestamp:

Nov 8, 2012, 2:27:54 PM (8 years ago)

Author:

tranquil

Message:

changed joint's stack pointer and internal stack

File:

• src/common/ByteValues.ma (modified) (1 diff)

src/common/ByteValues.ma

@@ -103 +103 @@
 axiom NotATwoBytesPointer: String.
 
-(* Fails if the address is not representable as a pair *)
-definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
- λp. OK … (list_to_pair … (bevals_of_pointer p) (refl …)).
+(* Should fail if the address is not representable as a pair
+   As we only have 16 bit addresses atm, it never fails *)
+definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
+ λp.list_to_pair … (bevals_of_pointer p) (refl …).
 (*
  λp. match p with [ mk_pointer pty pbl pok poff ⇒