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

Finished demo script for tomorrow.

File size:
1.3 KB

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.