source:
Deliverables/D4.1/Matita/Bool.ma
@
281
Last change on this file since 281 was 281, 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 | ]. |
31 | ||
32 | nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ | |
33 | match b with | |
[260] | 34 | [ true ⇒ |
[228] | 35 | match c with |
[260] | 36 | [ false ⇒ true |
37 | | true ⇒ false | |
[228] | 38 | ] |
[260] | 39 | | false ⇒ |
[228] | 40 | match c with |
[260] | 41 | [ false ⇒ false |
42 | | true ⇒ true | |
[228] | 43 | ] |
44 | ]. | |
45 | ||
[268] | 46 | interpretation "Bool" 'or a b = (inclusive_disjunction a b). |
47 | ||
[228] | 48 | nlet rec negation (b: Bool) on b ≝ |
49 | match b with | |
[260] | 50 | [ true ⇒ false |
51 | | false ⇒ true | |
[281] | 52 | ]. |
[260] | 53 |
Note: See TracBrowser
for help on using the repository browser.