Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Termination.TermCheck

Synopsis

Documentation

termDecl :: Declaration -> TCM Result Source #

Entry point: Termination check a single declaration.

Precondition: envMutualBlock must be set correctly.

termMutual Source #

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.