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('if' b 'then' t 'else' 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
        ]
    ].

interpretation "Bool" 'or a b = (inclusive_disjunction a b).

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