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

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

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File size: 1009 bytes
Line 
1include "logic/pts.ma".
2
3ninductive Bool: Type[0] ≝
4  True: Bool
5| False: Bool.
6
7nlet 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   
13notation "hvbox(b ? t : f)"
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
22      [ True ⇒ c
23      | False ⇒ False
24      ].
25   
26nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝
27  match b with
28    [ True ⇒ True
29    | False ⇒ c
30    ].
31
32nlet 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
46nlet rec negation (b: Bool) on b ≝
47  match b with
48    [ True ⇒ False
49    | False ⇒ True
50    ]. 
51 
Note: See TracBrowser for help on using the repository browser.