 Timestamp:
 Jul 13, 2011, 5:12:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/I8051.ma
r1060 r1066 115 115 bitvector_of_nat ? (nat_of_register register). 116 116 117 definition compare_register: Register → Register → Compare ≝117 definition compare_register: Register → Register → compare ≝ 118 118 λr, s: Register. 119 119 let r_as_nat ≝ nat_of_register r in 120 120 let s_as_nat ≝ nat_of_register s in 121 121 match eqb r_as_nat s_as_nat with 122 [ true ⇒ Compare_Equal122 [ true ⇒ compare_equal 123 123  false ⇒ 124 124 match ltb r_as_nat s_as_nat with 125 [ true ⇒ Compare_Less126  false ⇒ Compare_Greater125 [ true ⇒ compare_less 126  false ⇒ compare_greater 127 127 ] 128 128 ].
Note: See TracChangeset
for help on using the changeset viewer.