<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.TypeChecking.Monad.Imports</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-TypeChecking-Monad-Imports.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Monad-Imports.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.TypeChecking.Monad.Imports</p></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><a href="#v:addImport">addImport</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:addImportCycleCheck">addImportCycleCheck</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><a href="#v:getImports">getImports</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>)</li><li class="src short"><a href="#v:isImported">isImported</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:getImportPath">getImportPath</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a>]</li><li class="src short"><a href="#v:visitModule">visitModule</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:ModuleInfo">ModuleInfo</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:setVisitedModules">setVisitedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:VisitedModules">VisitedModules</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:getVisitedModules">getVisitedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:VisitedModules">VisitedModules</a></li><li class="src short"><a href="#v:isVisited">isVisited</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:getVisitedModule">getVisitedModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Base.html#t:ModuleInfo">ModuleInfo</a>)</li><li class="src short"><a href="#v:getDecodedModules">getDecodedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DecodedModules">DecodedModules</a></li><li class="src short"><a href="#v:setDecodedModules">setDecodedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:DecodedModules">DecodedModules</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:getDecodedModule">getDecodedModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a>, <a href="Agda-Utils-Time.html#t:ClockTime">ClockTime</a>))</li><li class="src short"><a href="#v:storeDecodedModule">storeDecodedModule</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a> -> <a href="Agda-Utils-Time.html#t:ClockTime">ClockTime</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:dropDecodedModule">dropDecodedModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:withImportPath">withImportPath</a> :: [<a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><a href="#v:checkForImportCycle">checkForImportCycle</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:addImport" class="def">addImport</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#addImport" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addImportCycleCheck" class="def">addImportCycleCheck</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-Monad-Imports.html#addImportCycleCheck" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getImports" class="def">getImports</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>)<a href="src/Agda-TypeChecking-Monad-Imports.html#getImports" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isImported" class="def">isImported</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Monad-Imports.html#isImported" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getImportPath" class="def">getImportPath</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a>]<a href="src/Agda-TypeChecking-Monad-Imports.html#getImportPath" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:visitModule" class="def">visitModule</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:ModuleInfo">ModuleInfo</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#visitModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setVisitedModules" class="def">setVisitedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:VisitedModules">VisitedModules</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#setVisitedModules" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getVisitedModules" class="def">getVisitedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:VisitedModules">VisitedModules</a><a href="src/Agda-TypeChecking-Monad-Imports.html#getVisitedModules" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isVisited" class="def">isVisited</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Monad-Imports.html#isVisited" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getVisitedModule" class="def">getVisitedModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Base.html#t:ModuleInfo">ModuleInfo</a>)<a href="src/Agda-TypeChecking-Monad-Imports.html#getVisitedModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getDecodedModules" class="def">getDecodedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DecodedModules">DecodedModules</a><a href="src/Agda-TypeChecking-Monad-Imports.html#getDecodedModules" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setDecodedModules" class="def">setDecodedModules</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:DecodedModules">DecodedModules</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#setDecodedModules" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getDecodedModule" class="def">getDecodedModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a>, <a href="Agda-Utils-Time.html#t:ClockTime">ClockTime</a>))<a href="src/Agda-TypeChecking-Monad-Imports.html#getDecodedModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:storeDecodedModule" class="def">storeDecodedModule</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a> -> <a href="Agda-Utils-Time.html#t:ClockTime">ClockTime</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#storeDecodedModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dropDecodedModule" class="def">dropDecodedModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#dropDecodedModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withImportPath" class="def">withImportPath</a> :: [<a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-Monad-Imports.html#withImportPath" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:checkForImportCycle" class="def">checkForImportCycle</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Monad-Imports.html#checkForImportCycle" class="link">Source</a></p><div class="doc"><p>Assumes that the first module in the import path is the module we are
worried about.
</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
