Last change
on this file since 290 was
268,
checked in by sacerdot, 10 years ago

 notation moved to proper places
 new function split on Vectors

File size:
1.3 KB

Line  

1  include "Bool.ma". 

2  include "Maybe.ma". 

3  

4  include "Universes.ma". 

5  

6  ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝ 

7  Left: A → Either A B 

8   Right: B → Either A B. 

9  

10  notation "hvbox(a break ⊎ b)" 

11  left associative with precedence 50 

12  for @{ 'disjoint_union $a $b }. 

13  interpretation "Either" 'disjoint_union A B = (Either A B). 

14  

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

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

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

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

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

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