Ignore:
Timestamp:
Nov 26, 2010, 9:35:28 PM (9 years ago)
Author:
sacerdot
Message:

More work on fetch.

File:
1 edited

Legend:

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

    r320 r322  
    147147nqed.
    148148
    149 ndefinition head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))).
     149ndefinition head: ∀A:Type[0]. ∀n. Vector A (S n) → A × (Vector A n)
     150≝ λA,n,v.
     151 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with
     152  [ Empty ⇒ λK.⊥
     153  | Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉
     154  ] (? : S ? = S ?).
     155//; ndestruct; //.
     156nqed.
     157
     158ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝
     159 λA,v. first … (head … v).
    150160   
    151161(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    159169    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
    160170    ].
    161    
     171
     172(*
    162173nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
    163174                      (n: Nat) (m: Nat)
     
    177188        ]
    178189    ]) ?.
    179    
     190*)
     191 
    180192nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
    181193                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
Note: See TracChangeset for help on using the changeset viewer.