Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Termination.TermCheck
Synopsis
termDecls :: [Declaration] -> TCM Result
type Result = [([QName], [Range])]
data DeBruijnPat
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
Produced by Haddock version 2.6.0