Ignore:
Timestamp:
Dec 16, 2010, 6:17:14 PM (11 years ago)
Author:
mulligan
Message:

Changes to get everything to compile.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Status.ma

    r362 r439  
    848848        λindirect: True.
    849849          let register ≝ get_register s [[ false; false; i ]] in
    850           let 〈 nu, nl 〉 ≝ split ? four four register in
     850          let 〈nu, nl〉 ≝ split ? four four register in
    851851          let bit_one ≝ get_index_v … nu one ? in
    852           let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    853           match bit_one with
    854             [ true ⇒
    855               let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
    856                 set_low_internal_ram s memory
    857             | false ⇒
    858               let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
    859                 set_high_internal_ram s memory
    860             ]
     852          let 〈ignore, three_bits〉 ≝ split ? one three nu in
     853            match bit_one with
     854              [ true ⇒
     855                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
     856                  set_low_internal_ram s memory
     857              | false ⇒
     858                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
     859                  set_high_internal_ram s memory
     860              ]
    861861      | REGISTER r ⇒ λregister: True. set_register s r v
    862862      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
Note: See TracChangeset for help on using the changeset viewer.