Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered




checkDecls :: [Declaration] -> TCM ()Source

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM ()Source

Type check a single declaration.

checkAxiom :: DefInfo -> Relevance -> 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 -> [Declaration] -> 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.

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

Type check a module.

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

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