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.