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

Safe Haskell | Safe-Infered

Agda.Termination.TermCheck

Synopsis

- termDecls :: [Declaration] -> TCM Result
- type Result = [TerminationError]
- data DeBruijnPat

# Documentation

termDecls :: [Declaration] -> TCM Result

Termination check a sequence of declarations.

type Result = [TerminationError]

The result of termination checking a module.

data DeBruijnPat

Termination check clauses

Instances

PrettyTCM DeBruijnPat |