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/Either.ma

    r260 r268  
    77  Left: A → Either A B
    88| Right: B → Either A B.
     9
     10notation "hvbox(a break ⊎ b)"
     11 left associative with precedence 50
     12for @{ 'disjoint_union $a $b }.
     13interpretation "Either" 'disjoint_union A B = (Either A B).
    914
    1015ndefinition is_left ≝
Note: See TracChangeset for help on using the changeset viewer.