--#include "../SET.alfa"
package OpBool where
open SET use Bool, True
true :: Bool
= true@_
false :: Bool
= false@_
not (x::Bool) :: Bool
= case x of {
(true) -> false@_;
(false) -> true@_;}
or (x::Bool)(y::Bool) :: Bool
= case x of {
(true) -> true@_;
(false) -> y;}
and (x::Bool)(y::Bool) :: Bool
= case x of {
(true) -> y;
(false) -> false@_;}
imp (x::Bool)(y::Bool) :: Bool
= case x of {
(true) -> y;
(false) -> true@_;}
iff (x::Bool)(y::Bool) :: Bool
= case y of {
(true) -> x;
(false) -> not x;}
existT (p::Bool)(q::True p -> Bool) :: Bool
= case p of {
(true) -> q tt@_;
(false) -> false@_;}
forallT (p::Bool)(q::True p -> Bool) :: Bool
= case p of {
(true) -> q tt@_;
(false) -> true@_;}
{-# Alfa hiding on
var "true" as "T" with symbolfont
var "false" as "^" with symbolfont
var "or" infix as "Ú" with symbolfont
var "and" infix as "Ù" with symbolfont
var "not" as "Ø" with symbolfont
var "imp" infix as "Þ" with symbolfont
var "iff" infix as "Û" with symbolfont
var "existT" as "$B" with symbolfont
var "forallT" as "\"B" with symbolfont
#-}