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

Agda.Termination.TermCheck

Synopsis

Documentation

Entry point: Termination check a single declaration.

type Result = [TerminationError] Source #

The result of termination checking a module. Must be a Monoid and have Singleton.

Patterns with variables as de Bruijn indices.