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

Last change on this file since 289 was 268, checked in by sacerdot, 9 years ago
  • notation moved to proper places
  • new function split on Vectors
File size: 1.3 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
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).
14
15ndefinition is_left ≝
16  λA, B: Type[0].
17  λe: Either A B.
18    match e with
19      [ Left l ⇒ true
20      | Right r ⇒ false
21      ].
22     
23ndefinition is_right ≝
24  λA, B: Type[0].
25  λe: Either A B.
26    match e with
27      [ Left l ⇒ false
28      | Right r ⇒ true
29      ].
30
31ndefinition either ≝
32  λA, B, C: Type[0].
33  λf: A → C.
34  λg: B → C.
35  λe: Either A B.
36    match e with
37      [ Left l ⇒ f l
38      | Right r ⇒ g r
39      ].
40     
41ndefinition map_left ≝
42  λA, B, C: Type[0].
43  λf: A → C.
44  λe: Either A B.
45    match e with
46      [ Left l ⇒ Left C B (f l)
47      | Right r ⇒ Right C B r
48      ].
49     
50ndefinition map_right ≝
51  λA, B, C: Type[0].
52  λf: B → C.
53  λe: Either A B.
54    match e with
55      [ Left l ⇒ Left A C l
56      | Right r ⇒ Right A C (f r)
57      ].
58     
59ndefinition map_both ≝
60  λA, B, C, D: Type[0].
61  λf: A → C.
62  λg: B → D.
63  λe: Either A B.
64    match e with
65      [ Left l ⇒ Left C D (f l)
66      | Right r ⇒ Right C D (g r)
67      ].
Note: See TracBrowser for help on using the repository browser.