Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (10 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/Matita/Bool.ma

    r246 r260  
    22
    33ninductive Bool: Type[0] ≝
    4   True: Bool
    5 | False: Bool.
     4  true: Bool
     5| false: Bool.
    66
    77nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝
    88  match b with
    9     [ True ⇒ t
    10     | False ⇒ f
     9    [ true ⇒ t
     10    | false ⇒ f
    1111    ].
    1212   
    … …  
    2020  λb, c: Bool.
    2121    match b with
    22       [ True ⇒ c
    23       | False ⇒ False
     22      [ true ⇒ c
     23      | false ⇒ false
    2424      ].
    2525   
    2626nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝
    2727  match b with
    28     [ True ⇒ True
    29     | False ⇒ c
     28    [ true ⇒ true
     29    | false ⇒ c
    3030    ].
    3131
    3232nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝
    3333  match b with
    34     [ True ⇒
     34    [ true ⇒
    3535      match c with
    36         [ False ⇒ True
    37         | True ⇒ False
     36        [ false ⇒ true
     37        | true ⇒ false
    3838        ]
    39     | False ⇒
     39    | false ⇒
    4040      match c with
    41         [ False ⇒ False
    42         | True ⇒ True
     41        [ false ⇒ false
     42        | true ⇒ true
    4343        ]
    4444    ].
    … …  
    4646nlet rec negation (b: Bool) on b ≝
    4747  match b with
    48     [ True ⇒ False
    49     | False ⇒ True
     48    [ true ⇒ false
     49    | false ⇒ true
    5050    ]. 
    5151 
Note: See TracChangeset for help on using the changeset viewer.