    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- IO handles: simple bindings to Haskell types and functions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module IO.Handle where

    open import Level using (Level)
    open import Data.Unit.Polymorphic.Base using (⊤)
    open import IO.Base using (IO; lift; lift′)

    private variable a : Level

    ------------------------------------------------------------------------
    -- Re-exporting types and constructors

    open import IO.Primitive.Handle as Prim public
      using ( BufferMode
            ; noBuffering
            ; lineBuffering
            ; blockBuffering
            ; Handle
            ; stdin
            ; stdout
            ; stderr
            )

    ------------------------------------------------------------------------
    -- Wrapping functions

    hSetBuffering : Handle → BufferMode → IO {a} ⊤
    hSetBuffering hdl bm = lift′ (Prim.hSetBuffering hdl bm)

    hGetBuffering : Handle → IO BufferMode
    hGetBuffering hdl = lift (Prim.hGetBuffering hdl)

    hFlush : Handle → IO {a} ⊤
    hFlush hdl = lift′ (Prim.hFlush hdl)