Changeset 1600 for src/ASM/I8051.ma
 Timestamp:
 Dec 13, 2011, 1:41:08 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/I8051.ma
r1515 r1600 5 5 include "ASM/ASM.ma". 6 6 include "ASM/Arithmetic.ma". 7 include "utilities/Compare.ma".8 7 include "joint/BEValues.ma". 9 8 include "ASM/BitVectorTrie.ma". … … 118 117 λregister. 119 118 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 in124 let s_as_nat ≝ nat_of_register s in125 match eqb r_as_nat s_as_nat with126 [ true ⇒ compare_equal127  false ⇒128 match ltb r_as_nat s_as_nat with129 [ true ⇒ compare_less130  false ⇒ compare_greater131 ]132 ].133 119 134 120 definition eq_Register: Register → Register → bool ≝
Note: See TracChangeset
for help on using the changeset viewer.