Safe Haskell	Safe-Inferred
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

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 #
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 #

The default termination depth.