Safe Haskell	None
Language	Haskell2010

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

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 details

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 #
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 -> () #
EmbPrj CutOff Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: CutOff -> S Int32 Source # icod_ :: CutOff -> S Int32 Source # value :: Int32 -> R CutOff Source #

The default termination depth.