Idris.ModTree

Definitions

record BuildMod : Type

Totality: total
Visibility: public export
Constructor: 

MkBuildMod : String -> ModuleIdent -> List ModuleIdent -> BuildMod

Projections:

.buildFile : BuildMod -> String

.buildNS : BuildMod -> ModuleIdent

.imports : BuildMod -> List ModuleIdent

Hint: 

Show BuildMod

.buildFile : BuildMod -> String

Visibility: public export

buildFile : BuildMod -> String

Visibility: public export

.buildNS : BuildMod -> ModuleIdent

Visibility: public export

buildNS : BuildMod -> ModuleIdent

Visibility: public export

.imports : BuildMod -> List ModuleIdent

Visibility: public export

imports : BuildMod -> List ModuleIdent

Visibility: public export

getBuildMods : Ref Ctxt Defs => Ref ROpts REPLOpts => FC -> List BuildMod -> String -> Core (List BuildMod)

Visibility: export

needsBuilding : Ref Ctxt Defs => Ref ROpts REPLOpts => String -> String -> List String -> Core Bool

Visibility: export

buildMods : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => FC -> Nat -> Nat -> List BuildMod -> Core (List Error)

Visibility: export

buildDeps : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref MD Metadata => Ref UST UState => Ref ROpts REPLOpts => String -> Core (List Error)

Visibility: export

buildAll : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => List String -> Core (List Error)

Visibility: export