Agda-2.3.0: 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 = [TerminationError]Source

The result of termination checking a module.

data DeBruijnPat Source

Termination check clauses

Instances