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

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

- data CutOff
  - = CutOff Int
  - | DontCutOff

# 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

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 #