Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2435 r2443  
    103103axiom NotATwoBytesPointer: String.
    104104
    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 *)
     107definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
     108 λp.list_to_pair … (bevals_of_pointer p) (refl …).
    108109(*
    109110 λp. match p with [ mk_pointer pty pbl pok poff ⇒
Note: See TracChangeset for help on using the changeset viewer.