Changeset 636 for Deliverables/D3.1/Csemantics/cerco/Vector.ma
 Timestamp:
 Mar 4, 2011, 6:20:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/Vector.ma
r535 r636 201 201 ]. 202 202 203 let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat) 204 (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝ 205 match v with 206 [ VEmpty ⇒ x 207  VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl) 208 ]. 209 203 210 let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0]) 204 211 (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
Note: See TracChangeset
for help on using the changeset viewer.