MeasureSets.hs

module Measures where

import Data.Set 

{-@ measure foo @-}
{-@ measure foo1 @-}

data F a = F a | E

foo1 :: F a -> Set a
foo1 (F x) = singleton x
foo1 E     = empty


foo :: F Int -> Int
foo (F x) = x + 1
foo E     = 0

-- bar = F