| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Termination.TermCheck
Synopsis
- termDecl :: Declaration -> TCM Result
- termMutual :: [QName] -> TCM Result
- type Result = [TerminationError]
Documentation
termDecl :: Declaration -> TCM Result Source #
Entry point: Termination check a single declaration.
Precondition: envMutualBlock must be set correctly.
Arguments
| :: [QName] | The function names defined in this block on top-level. (For error-reporting only.) |
| -> TCM Result |
Entry point: Termination check the current mutual block.
type Result = [TerminationError] Source #
The result of termination checking a module.
Must be a Monoid and have Singleton.