module Measures where

{-@ data Wrapper a <p :: a -> Bool, r :: a -> a -> Bool > 
    = Wrap (rgref_ref :: a<p>) @-}
data Wrapper a = Wrap (a)

-- Two measures
{-@ measure fwdextends :: Int -> Int -> Bool @-}
{-@ measure actionP :: Int -> Bool @-}

{-@ data Wrapper2  = Wrapper2 (unwrapper :: (Wrapper<{\x -> (true)},{\x y -> (fwdextends y x)}> Int )) @-}
{- data Wrapper2  = Wrapper2 (unwrapper :: (Wrapper<{\x -> (actionP x)},{\x y -> (true)}> Int )) @-}
data Wrapper2  = Wrapper2 (Wrapper (Int) )