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

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File size:
1009 bytes

Line  

1  include "logic/pts.ma". 

2  

3  ninductive Bool: Type[0] ≝ 

4  True: Bool 

5   False: Bool. 

6  

7  nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝ 

8  match b with 

9  [ True ⇒ t 

10   False ⇒ f 

11  ]. 

12  

13  notation "hvbox(b ? t : f)" 

14  non associative with precedence 83 

15  for @{ 'if_then_else $b $t $f }. 

16  

17  interpretation "If_then_else" 'if_then_else b t f = (if_then_else ? b t f). 

18  

19  ndefinition conjunction ≝ 

20  λb, c: Bool. 

21  match b with 

22  [ True ⇒ c 

23   False ⇒ False 

24  ]. 

25  

26  nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝ 

27  match b with 

28  [ True ⇒ True 

29   False ⇒ c 

30  ]. 

31  

32  nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ 

33  match b with 

34  [ True ⇒ 

35  match c with 

36  [ False ⇒ True 

37   True ⇒ False 

38  ] 

39   False ⇒ 

40  match c with 

41  [ False ⇒ False 

42   True ⇒ True 

43  ] 

44  ]. 

45  

46  nlet rec negation (b: Bool) on b ≝ 

47  match b with 

48  [ True ⇒ False 

49   False ⇒ True 

50  ]. 

51  

Note: See
TracBrowser
for help on using the repository browser.