dk_bool.dk

#NAME dk_bool.

(; Bool ;)
(; Declaration ;)
bool : cc.uT.
def Bool : Type := cc.eT bool.

(; Constructors ;)
true : Bool.
false : Bool.

(; Pattern-matching ;)
def match :
  P : (Bool -> cc.uT) ->
  cc.eT (P true) ->
  cc.eT (P false) ->
  b : Bool ->
  cc.eT (P b).
[Ht] match _ Ht _ true --> Ht
[Hf] match _ _ Hf false --> Hf.

(; Operations ;)
(; polymorphic if .. then .. else .. ;)
def ite :
  A : cc.uT ->
  Bool ->
  cc.eT A ->
  cc.eT A ->
  cc.eT A.
[A,x,y,b]
    ite A b x y
      -->
    match (b : Bool => A) x y b.

(; boolean if .. then .. else .. ;)
def iteb : Bool -> Bool -> Bool -> Bool
     := ite bool.

(; negation ;)
def not : Bool -> Bool.
[b] not b --> iteb b false true.

(; binary operators ;)
def and : Bool -> Bool -> Bool.
[x,y] and x y --> iteb x y false.

def or : Bool -> Bool -> Bool.
[x,y] or x y --> iteb x true y.

def xor : Bool -> Bool -> Bool.
[x,y] xor x y --> iteb x (not y) y.

def imp : Bool -> Bool -> Bool.
[x,y] imp x y --> iteb x y true.

def eqv : Bool -> Bool -> Bool.
[x,y] eqv x y --> iteb x y (not y).