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

Safe HaskellSafe-Inferred
LanguageHaskell98

Agda.Termination.CutOff

Description

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.

Synopsis

Documentation

data CutOff Source

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