source: Deliverables/D4.1/Matita/Bool.ma @ 334

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

More added.

File size: 1.1 KB
RevLine 
[246]1include "Universes.ma".
[228]2
3ninductive Bool: Type[0] ≝
[260]4  true: Bool
5| false: Bool.
[228]6
7nlet 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]13notation "hvbox('if' b 'then' t 'else' f)"
[228]14  non associative with precedence 83
15  for @{ 'if_then_else $b $t $f }.
16 
17interpretation "If_then_else" 'if_then_else b t f = (if_then_else ? b t f).
18
19ndefinition conjunction ≝
20  λb, c: Bool.
21    match b with
[260]22      [ true ⇒ c
23      | false ⇒ false
[228]24      ].
25   
26nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝
27  match b with
[260]28    [ true ⇒ true
29    | false ⇒ c
[228]30    ].
[334]31   
32ncheck inclusive_disjunction.
[228]33
34nlet 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]48interpretation "Bool" 'or a b = (inclusive_disjunction a b).
49
[228]50nlet 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.