Safe Haskell	Safe
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 Source # (/=) :: CutOff -> CutOff -> Bool Source #
Ord CutOff Source #
Instance details Defined in Agda.Termination.CutOff Methods compare :: CutOff -> CutOff -> Ordering Source # (<) :: CutOff -> CutOff -> Bool Source # (<=) :: CutOff -> CutOff -> Bool Source # (>) :: CutOff -> CutOff -> Bool Source # (>=) :: CutOff -> CutOff -> Bool Source # max :: CutOff -> CutOff -> CutOff Source # min :: CutOff -> CutOff -> CutOff Source #
Show CutOff Source #
Instance details Defined in Agda.Termination.CutOff Methods showsPrec :: Int -> CutOff -> ShowS Source # show :: CutOff -> String Source # showList :: [CutOff] -> ShowS Source #
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 #