1 2module Agda.TypeChecking.Rules.Decl where 3 4import Agda.Syntax.Info (ModuleInfo) 5import Agda.Syntax.Abstract 6import Agda.TypeChecking.Monad.Base (TCM) 7 8checkDecls :: [Declaration] -> TCM () 9checkDecl :: Declaration -> TCM () 10checkSectionApplication :: ModuleInfo -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM () 11