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

Last change on this file since 259 was 247, checked in by mulligan, 10 years ago

Changes to get directory to compile.
File size: 1.2 KB
Line 
1include "Bool.ma".
2include "Maybe.ma".
3
4include "Universes.ma".
5
6ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝
7  Left: A → Either A B
8| Right: B → Either A B.
9
10ndefinition is_left ≝
11  λA, B: Type[0].
12  λe: Either A B.
13    match e with
14      [ Left l ⇒ True
15      | Right r ⇒ False
16      ].
17     
18ndefinition is_right ≝
19  λA, B: Type[0].
20  λe: Either A B.
21    match e with
22      [ Left l ⇒ False
23      | Right r ⇒ True
24      ].
25
26ndefinition either ≝
27  λA, B, C: Type[0].
28  λf: A → C.
29  λg: B → C.
30  λe: Either A B.
31    match e with
32      [ Left l ⇒ f l
33      | Right r ⇒ g r
34      ].
35     
36ndefinition map_left ≝
37  λA, B, C: Type[0].
38  λf: A → C.
39  λe: Either A B.
40    match e with
41      [ Left l ⇒ Left C B (f l)
42      | Right r ⇒ Right C B r
43      ].
44     
45ndefinition map_right ≝
46  λA, B, C: Type[0].
47  λf: B → C.
48  λe: Either A B.
49    match e with
50      [ Left l ⇒ Left A C l
51      | Right r ⇒ Right A C (f r)
52      ].
53     
54ndefinition map_both ≝
55  λA, B, C, D: Type[0].
56  λf: A → C.
57  λg: B → D.
58  λe: Either A B.
59    match e with
60      [ Left l ⇒ Left C D (f l)
61      | Right r ⇒ Right C D (g r)
62      ].
Note: See TracBrowser for help on using the repository browser.