Changeset 1066 for src/ASM/I8051.ma


Ignore:
Timestamp:
Jul 13, 2011, 5:12:10 PM (9 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1060 r1066  
    115115    bitvector_of_nat ? (nat_of_register register).
    116116
    117 definition compare_register: Register → Register → Compare ≝
     117definition compare_register: Register → Register → compare ≝
    118118  λr, s: Register.
    119119    let r_as_nat ≝ nat_of_register r in
    120120    let s_as_nat ≝ nat_of_register s in
    121121      match eqb r_as_nat s_as_nat with
    122       [ true ⇒ Compare_Equal
     122      [ true ⇒ compare_equal
    123123      | false ⇒
    124124        match ltb r_as_nat s_as_nat with
    125         [ true ⇒ Compare_Less
    126         | false ⇒ Compare_Greater
     125        [ true ⇒ compare_less
     126        | false ⇒ compare_greater
    127127        ]
    128128      ].
Note: See TracChangeset for help on using the changeset viewer.