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
terGetHaveInlinedWith
terSetHaveInlinedWith
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
patternDepth
unusedVar
class UsableSizeVars a
type MaskedDeBruijnPatterns
data Masked a
masked
notMasked
data CallPath
terSetSizeDepth