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

Agda.Termination.TermCheck

Synopsis

Documentation

termDecls :: [Declaration] -> TCM ResultSource

Termination check a sequence of declarations.

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

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 Source

Termination check clauses

Instances