Agda.Termination.TermCheck

valuetermDecl :: Declaration -> TCM Result

Entry point: Termination check a single declaration.

Precondition: envMutualBlock must be set correctly.

valuetermMutual

:: [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.

typetype Result = [TerminationError]

The result of termination checking a module. Must be a Monoid and have Singleton.