source: Deliverables/D4.1/Matita/Either.ma @ 374

Last change on this file since 374 was 357, checked in by sacerdot, 9 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 1.3 KB
Line 
1include "Bool.ma".
2
3ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝
4  Left: A → Either A B
5| Right: B → Either A B.
6
7notation "hvbox(a break ⊎ b)"
8 left associative with precedence 50
9for @{ 'disjoint_union $a $b }.
10interpretation "Either" 'disjoint_union A B = (Either A B).
11
12ndefinition is_left ≝
13  λA, B: Type[0].
14  λe: Either A B.
15    match e with
16      [ Left l ⇒ true
17      | Right r ⇒ false
18      ].
19     
20ndefinition is_right ≝
21  λA, B: Type[0].
22  λe: Either A B.
23    match e with
24      [ Left l ⇒ false
25      | Right r ⇒ true
26      ].
27
28ndefinition either ≝
29  λA, B, C: Type[0].
30  λf: A → C.
31  λg: B → C.
32  λe: Either A B.
33    match e with
34      [ Left l ⇒ f l
35      | Right r ⇒ g r
36      ].
37     
38ndefinition map_left ≝
39  λA, B, C: Type[0].
40  λf: A → C.
41  λe: Either A B.
42    match e with
43      [ Left l ⇒ Left C B (f l)
44      | Right r ⇒ Right C B r
45      ].
46     
47ndefinition map_right ≝
48  λA, B, C: Type[0].
49  λf: B → C.
50  λe: Either A B.
51    match e with
52      [ Left l ⇒ Left A C l
53      | Right r ⇒ Right A C (f r)
54      ].
55     
56ndefinition map_both ≝
57  λA, B, C, D: Type[0].
58  λf: A → C.
59  λg: B → D.
60  λe: Either A B.
61    match e with
62      [ Left l ⇒ Left C D (f l)
63      | Right r ⇒ Right C D (g r)
64      ].
Note: See TracBrowser for help on using the repository browser.