source: Deliverables/D4.1/Demo-March-2011/matita/Either.ma @ 644

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

Committed files for demo on Friday. Binary search works with O'Caml emulator. Need to check with submitted version of Matita emulator.

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.