Changeset 746 for src/ASM


Ignore:
Timestamp:
Apr 8, 2011, 11:51:38 AM (10 years ago)
Author:
mulligan
Message:

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r724 r746  
    105105  | RegisterDPH ⇒ 35
    106106  ].
     107 
     108definition physical_register_count ≝ 36.
     109
     110definition word_of_register: Register → Word ≝
     111  λregister.
     112    bitvector_of_nat ? (nat_of_register register).
    107113
    108114definition compare_register: Register → Register → Compare ≝
  • src/ASM/Util.ma

    r715 r746  
    115115  λm, n: nat.
    116116    leb n m.
     117   
     118(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
     119let rec eq_nat (n: nat) (m: nat) on n: bool ≝
     120  match n with
     121  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
     122  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     123  ].
    117124
    118125(* dpm: conflicts with library definitions
Note: See TracChangeset for help on using the changeset viewer.