Agda.TypeChecking.Monad.SizedTypes

Testing for type Size

data BoundedSize

class IsSizeType a

isSizeTypeTest

getBuiltinDefName

getBuiltinSize

isSizeNameTest

isSizeNameTestRaw

haveSizedTypes

builtinSizeHook

Constructors

sizeSort

sizeUniv

sizeType_

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