Line | |
---|

1 | include "Bool.ma". |
---|

2 | |
---|

3 | ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝ |
---|

4 | Left: A → Either A B |
---|

5 | | Right: B → Either A B. |
---|

6 | |
---|

7 | notation "hvbox(a break ⊎ b)" |
---|

8 | left associative with precedence 50 |
---|

9 | for @{ 'disjoint_union $a $b }. |
---|

10 | interpretation "Either" 'disjoint_union A B = (Either A B). |
---|

11 | |
---|

12 | ndefinition 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 | |
---|

20 | ndefinition 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 | |
---|

28 | ndefinition 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 | |
---|

38 | ndefinition 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 | |
---|

47 | ndefinition 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 | |
---|

56 | ndefinition 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.