Idris.Env

Reexports

Definitions

record EnvDesc : Type

  Environment variable used by Idris2 compiler

Totality: total
Visibility: public export
Constructor: 

MkEnvDesc : String -> String -> EnvDesc

Projections:

.help : EnvDesc -> String

.name : EnvDesc -> String

.name : EnvDesc -> String

Totality: total
Visibility: public export

name : EnvDesc -> String

Totality: total
Visibility: public export

.help : EnvDesc -> String

Totality: total
Visibility: public export

help : EnvDesc -> String

Totality: total
Visibility: public export

envs : List EnvDesc

  All environment variables used by Idris2 compiler

Totality: total
Visibility: public export

envNames : List String

Totality: total
Visibility: public export

idrisGetEnv : HasIO io => (name : String) -> {auto 0 _ : IsJust (find (\{arg:0} => name == {arg:0}) envNames)} -> io (Maybe String)

  Query documented environment variable

Totality: total
Visibility: public export