Ignore:
Timestamp:
Dec 2, 2010, 11:53:49 AM (9 years ago)
Author:
sacerdot
Message:

Less ambiguous definitions.

File:
1 edited

Legend:

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

    r357 r362  
    2424(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2525
     26(*
    2627ndefinition get_index_bv ≝
    2728  λn: Nat.
     
    2930  λm: Nat.
    3031  λp: m < n.
    31     get_index Bool n b m p.
     32    get_index_bv Bool n b m p.
    3233   
    3334interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
     
    4647  λm: Nat.
    4748    drop Bool n b m.
     49*)
    4850
    4951(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    5153(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    5254
    53 ndefinition zero ≝
    54   λn: Nat.
    55     ((replicate Bool n false): BitVector n).
    56    
    57 ndefinition max ≝
    58   λn: Nat.
    59     ((replicate Bool n true): BitVector n).
    60    
     55ndefinition zero: ∀n:Nat. BitVector n ≝
     56  λn: Nat. replicate Bool n false.
     57   
     58ndefinition max: ∀n:Nat. BitVector n ≝
     59  λn: Nat. replicate Bool n true.
     60
     61(*
    6162ndefinition append ≝
    6263  λm, n: Nat.
     
    6465  λc: BitVector n.
    6566    append Bool m n b c.
    66    
     67*)
     68 
    6769ndefinition pad ≝
    6870  λm, n: Nat.
     
    7577(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    7678
     79(*
    7780ndefinition reverse ≝
    7881  λn: Nat.
     
    8487  λb: BitVector n.
    8588    length Bool n b.
     89*)
    8690
    8791(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    126130(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    127131
     132(*
    128133ndefinition rotate_left_bv ≝
    129134  λn, m: Nat.
     
    147152  λc: Bool.
    148153    shift_right Bool n m b c.
    149    
     154*)
     155 
    150156(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    151157(* Conversions to and from lists and natural numbers.                         *)
    152158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    153159
     160(*
    154161ndefinition list_of_bitvector ≝
    155162  λn: Nat.
     
    160167  λl: List Bool.
    161168    vector_of_list Bool l.
     169*)
    162170
    163171nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
     
    194202  let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
    195203  let size ≝ length ? biglist in
    196   let bitvector ≝ bitvector_of_list biglist in
     204  let bitvector ≝ vector_of_list ? biglist in
    197205  let difference ≝ n - size in
    198206   less_than_or_equal_b_elim …
Note: See TracChangeset for help on using the changeset viewer.