Changeset 268 for Deliverables/D4.1/Matita/Either.ma
 Timestamp:
 Nov 23, 2010, 5:44:42 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Either.ma
r260 r268 7 7 Left: A → Either A B 8 8  Right: B → Either A B. 9 10 notation "hvbox(a break ⊎ b)" 11 left associative with precedence 50 12 for @{ 'disjoint_union $a $b }. 13 interpretation "Either" 'disjoint_union A B = (Either A B). 9 14 10 15 ndefinition is_left ≝
Note: See TracChangeset
for help on using the changeset viewer.