FancySum.idr

module OpenSums

data FancySum a = Bar Integer
                | Baz
                | More a


FancySumFlat : Type
FancySumFlat = FancySum Void

baz : FancySumFlat
baz = the FancySumFlat Baz

total
gaz : Integer
gaz = case baz of
           Bar i  => i
           Baz    => -1

data Pet = Cat | Dog

FancySumPro : Type
FancySumPro = FancySum Pet

bazPro : FancySumPro
bazPro = the FancySumPro Baz

total
gazPro : Integer
gazPro = case bazPro of
              Bar i  => i
              Baz    => -1