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

Safe HaskellNone

Agda.Termination.TermCheck

Synopsis

Documentation

termDecl :: Declaration -> TCM ResultSource

Termination check a single declaration.

type Result = [TerminationError]Source

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

data DeBruijnPat Source

Termination check clauses

Instances