Go backward to Sum Domains Go up to Top Go forward to Sum Domains

Sum Domains

Truth values as disjoint union

Domain Tr = TT + FF

where TT = Unit and FF = Unit

Operations

true = inTT()
false = inFF()
not(t) =
    cases t of
        isTT() -> inFF()
        isFF() -> inTT()
    end
or(t, u) =
    cases t of
        isTT() -> inTT()
        isFF() -> cases u of
            isTT() -> inTT()
            isFF() -> inFF()
    end
end
(t -> e [] f) = cases t of
    isTT() -> e
    isFF() -> f
end