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

Produced by Haddock version 2.6.0