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.