liquidhaskell-0.8.2.0: tests/todo/T1094_Lib.hs

{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--exactdc"     @-}

module T1094_Lib where

import Language.Haskell.Liquid.ProofCombinators

{-@ data Iso a b = Iso { to   :: a -> b
                       , from :: b -> a
                       , tof  :: y:b -> { to (from y) == y }
                       , fot  :: x:a -> { from (to x) == x }
                       }
@-}

data Iso a b = Iso { to   :: a -> b
                   , from :: b -> a
                   , tof  :: b -> Proof
                   , fot  :: a -> Proof
                   }