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

Last change on this file since 232 was 232, checked in by mulligan, 9 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.