include "Universes.ma".

ninductive Bool: Type[0] ≝
  True: Bool
| False: Bool.

nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝
  match b with
    [ True ⇒ t
    | False ⇒ f
    ].
    
notation "hvbox(b ? t : f)"
  non associative with precedence 83
  for @{ 'if_then_else $b $t $f }.
  
interpretation "If_then_else" 'if_then_else b t f = (if_then_else ? b t f).

ndefinition conjunction ≝
  λb, c: Bool.
    match b with
      [ True ⇒ c
      | False ⇒ False
      ].
    
nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝
  match b with
    [ True ⇒ True
    | False ⇒ c
    ].

nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝
  match b with
    [ True ⇒
      match c with
        [ False ⇒ True
        | True ⇒ False
        ]
    | False ⇒
      match c with
        [ False ⇒ False
        | True ⇒ True
        ]
    ].

nlet rec negation (b: Bool) on b ≝
  match b with
    [ True ⇒ False
    | False ⇒ True
    ].