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

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

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 1.2 KB
Line 
1include "Bool.ma".
2include "Maybe.ma".
3
4include "logic/pts.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.