Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (10 years ago)
Author:
sacerdot
Message:
  • notation moved to proper places
  • new function split on Vectors
File:
1 edited

Legend:

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

    r246 r268  
    22
    33nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
    4 {
    5   first: A;
     4{ first: A;
    65  second: B
    76}.
    87
    9 notation "(l,r)"
    10   non associative with precedence 90
    11   for @{ 'cartesian $l $r }.
    12  
    13 interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r).
     8interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
     9interpretation "Cartesian" 'product A B = (Cartesian A B).
Note: See TracChangeset for help on using the changeset viewer.