summaryrefslogtreecommitdiff
path: root/src/full/Agda/Termination/CutOff.hs
blob: 97cb823336704b7e775ed81e284dcdbbea002d7c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
-- | 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.

module Agda.Termination.CutOff where

-- | Cut off structural order comparison at some depth in termination checker?

data CutOff
  = CutOff Int -- ^ @c >= 0@ means: record decrease up to including @c+1@.
  | DontCutOff
  deriving (Eq, Ord)

instance Show CutOff where
  show (CutOff k) = show k
  show DontCutOff = "∞"

-- That's it!