    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Miscellanous information about the system environment
    ------------------------------------------------------------------------

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

    module System.Environment where

    open import IO using (IO; lift; run; ignore)
    open import Data.List.Base using (List)
    open import Data.Maybe.Base using (Maybe)
    open import Data.Product.Base using (_×_)
    open import Data.String.Base using (String)
    open import Data.Unit.Polymorphic using (⊤)
    open import Foreign.Haskell.Coerce

    import System.Environment.Primitive as Prim

    getArgs : IO (List String)
    getArgs = lift Prim.getArgs

    getProgName : IO String
    getProgName = lift Prim.getProgName

    lookupEnv : String → IO (Maybe String)
    lookupEnv var = lift (coerce (Prim.lookupEnv var))

    setEnv : String → String → IO ⊤
    setEnv var val = ignore (lift (Prim.setEnv var val))

    unsetEnv : String → IO ⊤
    unsetEnv var = ignore (lift (Prim.unsetEnv var))

    withArgs : ∀ {a} {A : Set a} → List String → IO A → IO A
    withArgs args io = lift (Prim.withArgs args (run io))

    withProgName : ∀ {a} {A : Set a} → String → IO A → IO A
    withProgName name io = lift (Prim.withProgName name (run io))

    getEnvironment : IO (List (String × String))
    getEnvironment = lift (coerce Prim.getEnvironment)