source:
Deliverables/D4.1/Matita/Bool.ma
@
334
Last change on this file since 334 was 334, checked in by , 10 years ago | |
---|---|
File size: 1.1 KB |
Rev | Line | |
---|---|---|
[246] | 1 | include "Universes.ma". |
[228] | 2 | |
3 | ninductive Bool: Type[0] ≝ | |
[260] | 4 | true: Bool |
5 | | false: Bool. | |
[228] | 6 | |
7 | nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝ | |
8 | match b with | |
[260] | 9 | [ true ⇒ t |
10 | | false ⇒ f | |
[228] | 11 | ]. |
12 | ||
[281] | 13 | notation "hvbox('if' b 'then' t 'else' f)" |
[228] | 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 | |
[260] | 22 | [ true ⇒ c |
23 | | false ⇒ false | |
[228] | 24 | ]. |
25 | ||
26 | nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝ | |
27 | match b with | |
[260] | 28 | [ true ⇒ true |
29 | | false ⇒ c | |
[228] | 30 | ]. |
[334] | 31 | |
32 | ncheck inclusive_disjunction. | |
[228] | 33 | |
34 | nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ | |
35 | match b with | |
[260] | 36 | [ true ⇒ |
[228] | 37 | match c with |
[260] | 38 | [ false ⇒ true |
39 | | true ⇒ false | |
[228] | 40 | ] |
[260] | 41 | | false ⇒ |
[228] | 42 | match c with |
[260] | 43 | [ false ⇒ false |
44 | | true ⇒ true | |
[228] | 45 | ] |
46 | ]. | |
47 | ||
[268] | 48 | interpretation "Bool" 'or a b = (inclusive_disjunction a b). |
49 | ||
[228] | 50 | nlet rec negation (b: Bool) on b ≝ |
51 | match b with | |
[260] | 52 | [ true ⇒ false |
53 | | false ⇒ true | |
[281] | 54 | ]. |
[260] | 55 |
Note: See TracBrowser
for help on using the repository browser.