Last change
on this file since 228 was
228,
checked in by mulligan, 9 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.