liquidhaskell-0.8.10.7: liquid-base/src/Foreign/Ptr.spec

module spec Foreign.Ptr where

import GHC.Ptr

invariant {v:Foreign.Ptr.Ptr a | 0 <= plen  v }
invariant {v:Foreign.Ptr.Ptr a | 0 <= pbase v }