Agda.Termination.CutOff

Defines CutOff type which is used in Options. This module's purpose is to eliminate the dependency of Base on the termination checker and everything it imports.

Documentation

data CutOff

Cut off structural order comparison at some depth in termination checker?

Constructors

CutOff Int

c >= 0 means: record decrease up to including c+1.

DontCutOff

Instances

Eq CutOff

Ord CutOff

Show CutOff