Agda-2.8.0: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Termination.CutOff

Description

Defines CutOff type which is used in Agda.Interaction.Options. This module's purpose is to eliminate the dependency of Agda.TypeChecking.Monad.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

Instances details
EmbPrj CutOff Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: CutOff -> S Word32 Source #

icod_ :: CutOff -> S Word32 Source #

value :: Word32 -> R CutOff Source #

Show CutOff Source # 
Instance details

Defined in Agda.Termination.CutOff

Methods

showsPrec :: Int -> CutOff -> ShowS #

show :: CutOff -> String #

showList :: [CutOff] -> ShowS #

NFData CutOff Source # 
Instance details

Defined in Agda.Termination.CutOff

Methods

rnf :: CutOff -> ()

Eq CutOff Source # 
Instance details

Defined in Agda.Termination.CutOff

Methods

(==) :: CutOff -> CutOff -> Bool

(/=) :: CutOff -> CutOff -> Bool

Ord CutOff Source # 
Instance details

Defined in Agda.Termination.CutOff

Methods

compare :: CutOff -> CutOff -> Ordering

(<) :: CutOff -> CutOff -> Bool

(<=) :: CutOff -> CutOff -> Bool

(>) :: CutOff -> CutOff -> Bool

(>=) :: CutOff -> CutOff -> Bool

max :: CutOff -> CutOff -> CutOff

min :: CutOff -> CutOff -> CutOff

defaultCutOff :: CutOff Source #

The default termination depth.