Ignore:
Timestamp:
Dec 1, 2010, 4:30:46 PM (9 years ago)
Author:
mulligan
Message:

No more axioms but the paralogisms.

File:
1 edited

Legend:

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

    r347 r351  
    44include "Arithmetic.ma".
    55include "List.ma".
    6 
    7 alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
    86
    97ndefinition sign_extension: Byte → Word ≝
     
    389387              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
    390388              let 〈nu, nl〉 ≝ split ? four four pc_bu in
    391               let bit ≝ cic:/matita/ng/Vector/get_index.fix(0,3,2) ? ? nl Z ? in
     389              let bit ≝ get_index_bv ? nl Z ? in
    392390              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
    393391              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
Note: See TracChangeset for help on using the changeset viewer.