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

Safe Haskell | None

Agda.Termination.TermCheck

Synopsis

- termDecl :: Declaration -> TCM Result
- type Result = [TerminationError]
- data DeBruijnPat

# Documentation

termDecl :: Declaration -> TCM Result

Termination check a single declaration.

type Result = [TerminationError]

The result of termination checking a module. Must be `Pointed` and a `Monoid`.

data DeBruijnPat

Termination check clauses

Instances

PrettyTCM DeBruijnPat |