5
5
import Agda.Syntax.Info (ModuleInfo)
6
import Agda.Syntax.Abstract (QName, Declaration, ModuleName, ModuleApplication)
6
import Agda.Syntax.Abstract (QName, Declaration, ModuleName, ModuleApplication, Ren)
7
7
import Agda.TypeChecking.Monad (TCM)
9
9
checkDecls :: [Declaration] -> TCM ()
10
10
checkDecl :: Declaration -> TCM ()
11
11
checkSectionApplication ::
12
12
ModuleInfo -> ModuleName -> ModuleApplication ->