Ignore:
Timestamp:
Feb 16, 2011, 4:25:00 PM (8 years ago)
Author:
campbell
Message:

Make stuff from D4.1 work with my copy of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/Vector.ma

    r475 r533  
    66include "basics/list.ma".
    77include "basics/bool.ma".
    8 include "basics/sums.ma".
     8include "basics/types.ma".
    99
    1010include "cerco/Util.ma".
     
    159159      | VCons o he tl ⇒ λK.
    160160        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〉
    162162        ]
    163163      ] (?: (S (m' + n)) = S (m' + n))].
     
    269269  λv: Vector A n.
    270270  λ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.
    272272
    273273(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.