Last change
on this file since 235 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  

1  include "Bool.ma". 

2  include "Maybe.ma". 

3  

4  include "logic/pts.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  ndefinition 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  

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

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

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

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

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