Changeset 533 for Deliverables/D3.1/Csemantics/cerco/Vector.ma
 Timestamp:
 Feb 16, 2011, 4:25:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/Vector.ma
r475 r533 6 6 include "basics/list.ma". 7 7 include "basics/bool.ma". 8 include "basics/ sums.ma".8 include "basics/types.ma". 9 9 10 10 include "cerco/Util.ma". … … 159 159  VCons o he tl ⇒ λK. 160 160 match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with 161 [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉161 [ pair v1 v2 ⇒ 〈he:::v1, v2〉 162 162 ] 163 163 ] (?: (S (m' + n)) = S (m' + n))]. … … 269 269 λv: Vector A n. 270 270 λq: Vector B n. 271 zip_with A B (A × B) n ( mk_pair A B) v q.271 zip_with A B (A × B) n (pair A B) v q. 272 272 273 273 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.