On 17 Oct 2010, at 05:21, Ben Franksen wrote: > I want to prove that > > f r == do > s1 <- readIORef r > r' <- newIORef s1 > x <- f r' > s3 <- readIORef r' > writeIORef r s3 > return x
That is not true. Consider the following function: g r1 r2 = writeIORef r1 0 >> writeIORef r2 1 >> readIORef r1 This function behaves differently depending on whether r1 and r2 are the same IORef or not. Therefore, the property you want to prove doesn't hold for the partially-applied function f = g r1._______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
