2
module Agda.Interaction.Imports where
4
import Agda.Syntax.Abstract.Name ( ModuleName )
5
import Agda.Syntax.Scope.Base ( Scope )
6
import Agda.TypeChecking.Monad.Base ( TCM )
7
import Data.Map ( Map )
9
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)