Ignore:
Timestamp:
Nov 30, 2010, 12:26:45 PM (10 years ago)
Author:
mulligan
Message:

Changes to execute_1 file. Changes to get everything type checking.

File:
1 edited

Legend:

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

    r331 r337  
    658658  λs: Status.
    659659  λr: BitVector three.
    660     let b ≝ get_index ? r Z ? in
    661     let c ≝ get_index ? r one ? in
    662     let d ≝ get_index ? r two ? in
     660    let b ≝ get_index_bv ? r Z ? in
     661    let c ≝ get_index_bv ? r one ? in
     662    let d ≝ get_index_bv ? r two ? in
    663663    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    664     let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
     664    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in
    665665    let offset ≝
    666666      if conjunction (negation r1) (negation r0) then
Note: See TracChangeset for help on using the changeset viewer.