|
Agda.TypeChecking.Rules.Decl |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Type check a sequence of declarations.
|
|
|
Type check a single declaration.
|
|
|
Type check an axiom.
|
|
|
Type check a primitive function declaration.
|
|
|
Check a pragma.
|
|
|
Type check a bunch of mutual inductive recursive definitions.
|
|
|
Type check the type signature of an inductive or recursive definition.
|
|
|
Check an inductive or recursive definition. Assumes the type has has been
checked and added to the signature.
|
|
|
Type check a module.
|
|
|
|
|
Check an application of a section.
|
|
|
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 |