Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 TelescopeSource
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.4.2