Ignore:
Timestamp:
Nov 11, 2010, 4:56:59 PM (9 years ago)
Author:
mulligan
Message:

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File:
1 edited

Legend:

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

    r231 r232  
    165165    ].
    166166
     167(*
    167168nlet rec from_list (A: Type[0]) (l: List A) on l ≝
    168169  match l return λl. Vector A (length A l) with
     
    172173    //.
    173174nqed.
     175*)
    174176
    175177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     
    248250  @.
    249251nqed.
    250 
    251 nlemma from_list_to_list_left_inverse:
    252   ∀A: Type[0].
    253   ∀l: List A.
    254     to_list A (length A l) (from_list A l) = l.
Note: See TracChangeset for help on using the changeset viewer.