Agda.TypeChecking.Monad.SizedTypes

# Testing for type `Size`

data BoundedSize

isSizeType

isSizeTypeTest

getBuiltinDefName

getBuiltinSize

isSizeNameTest

isSizeNameTestRaw

# Constructors

sizeType

sizeSucName

sizeSuc

sizeSuc_

sizeMax

# Viewing and unviewing sizes

data SizeView

sizeView

type Offset

data DeepSizeView

data SizeViewComparable a

sizeViewComparable

sizeViewSuc_

sizeViewPred

sizeViewOffset

removeSucs

unSizeView

unDeepSizeView

# View on sizes where maximum is pulled to the top

type SizeMaxView

maxViewMax

maxViewCons

sizeViewComparableWithMax

maxViewSuc_

unMaxView