Changeset 260 for Deliverables/D4.1/Matita/Bool.ma
- Timestamp:
- Nov 23, 2010, 2:30:10 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Bool.ma
r246 r260 2 2 3 3 ninductive Bool: Type[0] ≝ 4 True: Bool5 | False: Bool.4 true: Bool 5 | false: Bool. 6 6 7 7 nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝ 8 8 match b with 9 [ True ⇒ t10 | False ⇒ f9 [ true ⇒ t 10 | false ⇒ f 11 11 ]. 12 12 … … 20 20 λb, c: Bool. 21 21 match b with 22 [ True ⇒ c23 | False ⇒ False22 [ true ⇒ c 23 | false ⇒ false 24 24 ]. 25 25 26 26 nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝ 27 27 match b with 28 [ True ⇒ True29 | False ⇒ c28 [ true ⇒ true 29 | false ⇒ c 30 30 ]. 31 31 32 32 nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ 33 33 match b with 34 [ True ⇒34 [ true ⇒ 35 35 match c with 36 [ False ⇒ True37 | True ⇒ False36 [ false ⇒ true 37 | true ⇒ false 38 38 ] 39 | False ⇒39 | false ⇒ 40 40 match c with 41 [ False ⇒ False42 | True ⇒ True41 [ false ⇒ false 42 | true ⇒ true 43 43 ] 44 44 ]. … … 46 46 nlet rec negation (b: Bool) on b ≝ 47 47 match b with 48 [ True ⇒ False49 | False ⇒ True48 [ true ⇒ false 49 | false ⇒ true 50 50 ]. 51 51
Note: See TracChangeset
for help on using the changeset viewer.