Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Monad.Imports
Synopsis
addImport
::
ModuleName
->
TCM
()
addImportCycleCheck
::
TopLevelModuleName
->
TCM
a ->
TCM
a
getImports
::
TCM
(
Set
ModuleName
)
isImported
::
ModuleName
->
TCM
Bool
getImportPath
::
TCM
[
TopLevelModuleName
]
visitModule
::
ModuleInfo
->
TCM
()
setVisitedModules
::
VisitedModules
->
TCM
()
getVisitedModules
::
TCM
VisitedModules
isVisited
::
TopLevelModuleName
->
TCM
Bool
getVisitedModule
::
TopLevelModuleName
->
TCM
(
Maybe
ModuleInfo
)
getDecodedModules
::
TCM
DecodedModules
setDecodedModules
::
DecodedModules
->
TCM
()
preserveDecodedModules
::
TCM
a ->
TCM
a
getDecodedModule
::
TopLevelModuleName
->
TCM
(
Maybe
(
Interface
,
ClockTime
))
storeDecodedModule
::
Interface
->
ClockTime
->
TCM
()
dropDecodedModule
::
TopLevelModuleName
->
TCM
()
withImportPath
:: [
TopLevelModuleName
] ->
TCM
a ->
TCM
a
checkForImportCycle
::
TCM
()
Documentation
addImport
::
ModuleName
->
TCM
()
Source
addImportCycleCheck
::
TopLevelModuleName
->
TCM
a ->
TCM
a
Source
getImports
::
TCM
(
Set
ModuleName
)
Source
isImported
::
ModuleName
->
TCM
Bool
Source
getImportPath
::
TCM
[
TopLevelModuleName
]
Source
visitModule
::
ModuleInfo
->
TCM
()
Source
setVisitedModules
::
VisitedModules
->
TCM
()
Source
getVisitedModules
::
TCM
VisitedModules
Source
isVisited
::
TopLevelModuleName
->
TCM
Bool
Source
getVisitedModule
::
TopLevelModuleName
->
TCM
(
Maybe
ModuleInfo
)
Source
getDecodedModules
::
TCM
DecodedModules
Source
setDecodedModules
::
DecodedModules
->
TCM
()
Source
preserveDecodedModules
::
TCM
a ->
TCM
a
Source
getDecodedModule
::
TopLevelModuleName
->
TCM
(
Maybe
(
Interface
,
ClockTime
))
Source
storeDecodedModule
::
Interface
->
ClockTime
->
TCM
()
Source
dropDecodedModule
::
TopLevelModuleName
->
TCM
()
Source
withImportPath
:: [
TopLevelModuleName
] ->
TCM
a ->
TCM
a
Source
checkForImportCycle
::
TCM
()
Source
Assumes that the first module in the import path is the module we are worried about.
Produced by
Haddock
version 2.6.0