Agda.Termination.TermCheck

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