Changeset 1600 for src/ASM/I8051.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:41:08 PM (8 years ago)
Author:
sacerdot
Message:

utilities and ASM ported to the new standard library

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1515 r1600  
    55include "ASM/ASM.ma".
    66include "ASM/Arithmetic.ma".
    7 include "utilities/Compare.ma".
    87include "joint/BEValues.ma".
    98include "ASM/BitVectorTrie.ma".
     
    118117  λregister.
    119118    bitvector_of_nat ? (nat_of_register register).
    120 
    121 definition compare_register: Register → Register → compare ≝
    122   λr, s: Register.
    123     let r_as_nat ≝ nat_of_register r in
    124     let s_as_nat ≝ nat_of_register s in
    125       match eqb r_as_nat s_as_nat with
    126       [ true ⇒ compare_equal
    127       | false ⇒
    128         match ltb r_as_nat s_as_nat with
    129         [ true ⇒ compare_less
    130         | false ⇒ compare_greater
    131         ]
    132       ].
    133119
    134120definition eq_Register: Register → Register → bool ≝
Note: See TracChangeset for help on using the changeset viewer.