Changeset 322 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 26, 2010, 9:35:28 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r320 r322 147 147 nqed. 148 148 149 ndefinition head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))). 149 ndefinition 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; //. 156 nqed. 157 158 ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝ 159 λA,v. first … (head … v). 150 160 151 161 (* ===================================== *) … … 159 169  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 160 170 ]. 161 171 172 (* 162 173 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 163 174 (n: Nat) (m: Nat) … … 177 188 ] 178 189 ]) ?. 179 190 *) 191 180 192 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) 181 193 (f: A → B → A) (x: A) (v: Vector B n) on v ≝
Note: See TracChangeset
for help on using the changeset viewer.