bool.ya

package bool where

def Bool: Type = #Bool

def Bool.True: Bool = #Bool.true
def Bool.False: Bool = #Bool.false

def Bool.eql: ∀ (x y: Bool) -> Bool = #Bool.eql
def Bool.lte: ∀ (x y: Bool) -> Bool = #Bool.lte
def Bool.lth: ∀ (x y: Bool) -> Bool = #Bool.lth
def Bool.gte: ∀ (x y: Bool) -> Bool = #Bool.gte
def Bool.gth: ∀ (x y: Bool) -> Bool = #Bool.gth


def Bool.and: ∀ (x y: Bool) -> Bool = #Bool.and
def Bool.or:  ∀ (x y: Bool) -> Bool = #Bool.or
def Bool.xor: ∀ (x y: Bool) -> Bool = #Bool.xor

def Bool.not: ∀ (x: Bool) -> Bool = #Bool.not

def Bool.neq (x y: Bool): Bool = Bool.not (Bool.eql x y)

def Bool.if (A: Type) (bool : Bool) (t f: A): A = (case bool) (λ _ => A) t f