Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (9 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File:
1 edited

Legend:

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

    r257 r260  
    5555ndefinition zero ≝
    5656  λn: Nat.
    57     ((replicate Bool n False): BitVector n).
     57    ((replicate Bool n false): BitVector n).
    5858   
    5959ndefinition max ≝
    6060  λn: Nat.
    61     ((replicate Bool n True): BitVector n).
     61    ((replicate Bool n true): BitVector n).
    6262   
    6363ndefinition append ≝
     
    7272  λm, n: Nat.
    7373  λb: BitVector n.
    74     let padding ≝ replicate Bool m False in
     74    let padding ≝ replicate Bool m false in
    7575      append Bool m n padding b.
    7676     
     
    173173        match rem with
    174174          [ Z ⇒ Empty Bool
    175           | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
     175          | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
    176176          ]
    177177      | S d ⇒
    178178        match rem with
    179           [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
    180           | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
     179          [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
     180          | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
    181181          ]
    182182      ].
     
    196196    [ Empty ⇒ Z
    197197    | Cons o hd tl ⇒
    198       let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
     198      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
    199199        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    200200    ].
Note: See TracChangeset for help on using the changeset viewer.