Ignore:
Timestamp:
Nov 24, 2010, 5:19:38 PM (10 years ago)
Author:
sacerdot
Message:

Notation moved to Cartesian.

File:
1 edited

Legend:

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

    r268 r279  
    88interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
    99interpretation "Cartesian" 'product A B = (Cartesian A B).
     10
     11notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     12 with precedence 10
     13for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
     14
     15(*ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).*)
     16
Note: See TracChangeset for help on using the changeset viewer.