Idris2Doc : Idris.Driver.Extra

Idris.Driver.Extra

(source)
Re-exports Idris.Driver with some private declarations.

`Idris.Driver` private items are visible here because of the common module
prefix.

Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.

Reexports

import public Idris.Driver

Definitions

updateEnv : Ref Ctxt Defs => Ref ROpts REPLOpts => Core ()
Visibility: export
splitPaths : String -> List1 String
Visibility: export