Agda-2.4.2.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Termination.TermCheck

Synopsis

Documentation

termDecl :: Declaration -> TCM Result

Entry point: Termination check a single declaration.

type Result = [TerminationError]

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

type DeBruijnPat = DeBruijnPat' Int

Patterns with variables as de Bruijn indices.