| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Termination.TermCheck

Synopsis

termDecls :: [Declaration] -> TCM Result
type Result = [([QName], [Range])]
data DeBruijnPat

Documentation

termDecls :: [Declaration] -> TCM Result | Source

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

PrettyTCM DeBruijnPat

Produced by Haddock version 2.4.2