Ignore:
Timestamp:
Nov 12, 2010, 4:51:45 PM (9 years ago)
Author:
mulligan
Message:

More functions on bitvectors written.

File:
1 edited

Legend:

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

    r236 r237  
    166166    ].
    167167
    168 (*
    169168nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    170169  match l return λl. Vector A (length A l) with
    171     [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
    172     | Cons hd tl ⇒ ? (hd :: (from_list A tl))
    173     ].
    174     //.
    175 nqed.
    176 *)
     170    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
     171    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
     172    ].
     173    nnormalize.
     174    //.
     175    //.
     176nqed.
    177177
    178178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
Note: See TracChangeset for help on using the changeset viewer.