Safe Haskell | None |
---|---|
Language | Haskell2010 |
- termDecl :: Declaration -> TCM Result
- termMutual :: [QName] -> TCM Result
- type Result = [TerminationError]
- type DeBruijnPat = DeBruijnPat' Int
Documentation
termDecl :: Declaration -> TCM Result Source #
Entry point: Termination check a single declaration.
Precondition: envMutualBlock
must be set correctly.
:: [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 #
type DeBruijnPat = DeBruijnPat' Int Source #
Patterns with variables as de Bruijn indices.