Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Rules.Decl

Synopsis

- checkDecls :: [Declaration] -> TCM ()
- checkDecl :: Declaration -> TCM ()
- checkAxiom :: DefInfo -> Relevance -> QName -> Expr -> TCM ()
- checkPrimitive :: DefInfo -> QName -> Expr -> TCM ()
- checkPragma :: Range -> Pragma -> TCM ()
- checkMutual :: MutualInfo -> [Declaration] -> TCM (Set QName)
- checkTypeSignature :: TypeSignature -> TCM ()
- checkSection :: ModuleInfo -> ModuleName -> Telescope -> [Declaration] -> TCM ()
- checkModuleArity :: ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope
- checkSectionApplication :: ModuleInfo -> ModuleName -> ModuleApplication -> Map QName QName -> Map ModuleName ModuleName -> TCM ()
- checkSectionApplication' :: ModuleInfo -> ModuleName -> ModuleApplication -> Map QName QName -> Map ModuleName ModuleName -> TCM ()
- checkImport :: ModuleInfo -> ModuleName -> TCM ()

# Documentation

checkDecls :: [Declaration] -> TCM ()

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM ()

Type check a single declaration.

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

Type check an axiom.

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

Type check a primitive function declaration.

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

Check a pragma.

checkMutual :: MutualInfo -> [Declaration] -> TCM (Set QName)

Type check a bunch of mutual inductive recursive definitions.

All definitions which have so far been assigned to the given mutual block are returned.

checkTypeSignature :: TypeSignature -> TCM ()

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

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

Type check a module.

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

checkSectionApplication :: ModuleInfo -> ModuleName -> ModuleApplication -> Map QName QName -> Map ModuleName ModuleName -> TCM ()

Check an application of a section.

checkSectionApplication' :: ModuleInfo -> ModuleName -> ModuleApplication -> Map QName QName -> Map ModuleName ModuleName -> TCM ()

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

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