Agda.TypeChecking.Rules.Decl

Synopsis

checkDecls :: [Declaration] -> TCM ()

checkDecl :: Declaration -> TCM ()

checkAxiom :: DefInfo -> QName -> Expr -> TCM ()

checkPrimitive :: DefInfo -> QName -> Expr -> TCM ()

checkPragma :: Range -> Pragma -> TCM ()

checkMutual :: DeclInfo -> [TypeSignature] -> [Definition] -> TCM ()

checkTypeSignature :: TypeSignature -> TCM ()

checkDefinition :: Definition -> TCM ()

checkSection :: ModuleInfo -> ModuleName -> Telescope -> [Declaration] -> TCM ()

checkModuleArity :: ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope

checkSectionApplication :: ModuleInfo -> ModuleName -> Telescope -> ModuleName -> [NamedArg Expr] -> Map QName QName -> Map ModuleName ModuleName -> TCM ()

checkImport :: ModuleInfo -> ModuleName -> TCM ()

Documentation

checkDecls :: [Declaration] -> TCM ()

Source

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM ()

Source

Type check a single declaration.

checkAxiom :: DefInfo -> QName -> Expr -> TCM ()

Source

Type check an axiom.

checkPrimitive :: DefInfo -> QName -> Expr -> TCM ()

Source

Type check a primitive function declaration.

checkPragma :: Range -> Pragma -> TCM ()

Source

Check a pragma.

checkMutual :: DeclInfo -> [TypeSignature] -> [Definition] -> TCM ()

Source

Type check a bunch of mutual inductive recursive definitions.

checkTypeSignature :: TypeSignature -> TCM ()

Source

Type check the type signature of an inductive or recursive definition.

checkDefinition :: Definition -> TCM ()

Source

Check an inductive or recursive definition. Assumes the type has has been checked and added to the signature.

checkSection :: ModuleInfo -> ModuleName -> Telescope -> [Declaration] -> TCM ()

Source

Type check a module.

checkModuleArity :: ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope

Source

checkSectionApplication :: ModuleInfo -> ModuleName -> Telescope -> ModuleName -> [NamedArg Expr] -> Map QName QName -> Map ModuleName ModuleName -> TCM ()

Source

Check an application of a section.

checkImport :: ModuleInfo -> ModuleName -> TCM ()

Source

Type check an import declaration. Actually doesn't do anything, since all the work is done when scope checking.

Produced by Haddock version 2.6.0