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

Committed files for demo on Friday. Binary search works with O'Caml emulator. Need to check with submitted version of Matita emulator.

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.