Ignore:
Timestamp:
Nov 22, 2010, 11:43:04 AM (9 years ago)
Author:
mulligan
Message:

More changes. Added datatype for addressing modes.

File:
1 edited

Legend:

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

    r246 r248  
    2323ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
    2424ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
     25ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))).
    2526
    2627(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    196197    | Cons o hd tl ⇒
    197198      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
    198         ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl
     199        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    199200    ].
Note: See TracChangeset for help on using the changeset viewer.