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

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

- data CutOff
  - = CutOff !Int
  - | DontCutOff
- defaultCutOff :: CutOff

# 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 #
NFData CutOff Source # |
Instance details Defined in Agda.Termination.CutOff Methods rnf :: 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 #
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 #

defaultCutOff :: CutOff Source #

The default termination depth.