Idris2Doc : Idris.Package.Extra

Idris.Package.Extra

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

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

Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.

Reexports

import public Idris.Package

Definitions

withWarnings : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => Core a -> Core a
  Emit captured warnings from inner scope and clear them
  afterwards (to avoid emitting them in some unrelated
  codepath later).

Visibility: export
runScript : Maybe (FC, String) -> Core ()
Visibility: export
addDeps : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => PkgDesc -> Core ()
  Add all dependencies (transitively) from the given package file into the
  context so modules from each is accessible during compilation.

Visibility: export