Register the given module as imported in the current state. Also recursively add its imports to the cumulative imports.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Imports
Synopsis
- value addImport
- value addImportCycleCheck
- value checkForImportCycle
- value dropDecodedModule
- value getDecodedModule
- value getDecodedModules
- value getImportPath
- value getPrettyVisitedModules
- value getVisitedModule
- value getVisitedModules
- value setDecodedModules
- value setVisitedModules
- value storeDecodedModule
- value visitModule
- value withImportPath
- PackageAgda-2.8.0.2
- Exports15
- LanguageHaskell2010
- LicenceMIT
- SourceImports.hs
Assumes that the first module in the import path is the module we are worried about.