Agda.Termination.TermCheck

Documentation

termDecls :: [Declaration] -> TCM Result

Termination check a sequence of declarations.

type Result = [([QName], [Range])]

The result of termination checking a module is a list of problematic mutual blocks (represented by the names of the functions in the block), along with the ranges for the problematic call sites (call site paths).

data DeBruijnPat

Termination check clauses

Instances

PrettyTCM DeBruijnPat