liquidhaskell-0.8.10.7: liquid-base/src/GHC/IO/Handle.spec

module spec GHC.IO.Handle where

hGetBuf :: GHC.IO.Handle.Handle -> GHC.Ptr.Ptr a -> n:Nat
        -> (GHC.Types.IO {v:Nat | v <= n})

hGetBufNonBlocking :: GHC.IO.Handle.Handle -> GHC.Ptr.Ptr a -> n:Nat
                   -> (GHC.Types.IO {v:Nat | v <= n})

hFileSize :: GHC.IO.Handle.Handle
          -> (GHC.Types.IO {v:Integer | v >= 0})