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('if' b 'then' t 'else' 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 | interpretation "Bool" 'or a b = (inclusive_disjunction a b). |
---|

47 | |
---|

48 | nlet rec negation (b: Bool) on b ≝ |
---|

49 | match b with |
---|

50 | [ true ⇒ false |
---|

51 | | false ⇒ true |
---|

52 | ]. |
---|

53 | |
---|

**Note:** See

TracBrowser
for help on using the repository browser.