Agda.Termination.Monad
type MutualNames
type Target
type Guarded
data TerEnv
defaultTerEnv
class MonadTer m
data TerM a
runTer
runTerDefault
MonadTCM
terGetGuardingTypeConstructors
terGetInlineWithFunctions
terGetUseDotPatterns
terSetUseDotPatterns
terGetSizeSuc
terGetCurrent
terSetCurrent
terGetSharp
terGetCutOff
terGetMutual
terGetUserNames
terGetTarget
terSetTarget
terGetDelayed
terSetDelayed
terGetMaskArgs
terSetMaskArgs
terGetMaskResult
terSetMaskResult
terGetPatterns
terSetPatterns
terRaise
terGetGuarded
terModifyGuarded
terSetGuarded
terUnguarded
terPiGuarded
terSizeDepth
terGetUsableVars
terModifyUsableVars
terSetUsableVars
terGetUseSizeLt
terModifyUseSizeLt
terSetUseSizeLt
withUsableVars
conUseSizeLt
projUseSizeLt
isProjectionButNotCoinductive
isCoinductiveProjection
type DeBruijnPats
type DeBruijnPat
data DeBruijnPat' a
patternDepth
unusedVar
raiseDBP
class UsableSizeVars a
type MaskedDeBruijnPats
data Masked a
masked
notMasked
data CallPath
terSetSizeDepth