Agda.Termination.Monad

type MutualNames

type Target

type Guarded

data TerEnv

defaultTerEnv

class MonadTer m

data TerM a

runTer

runTerDefault

Termination monad is a MonadTCM.

Modifiers and accessors for the termination environment in the monad.

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

De Bruijn patterns.

type DeBruijnPats

type DeBruijnPat

data DeBruijnPat' a

patternDepth

unusedVar

raiseDBP

class UsableSizeVars a

Masked patterns (which are not eligible for structural descent, only for size descent)

type MaskedDeBruijnPats

data Masked a

masked

notMasked

Call pathes

data CallPath

Size depth estimation

terSetSizeDepth