Agda.TypeChecking.Monad.SizedTypes
Size
data BoundedSize
class IsSizeType a
isSizeTypeTest
getBuiltinDefName
getBuiltinSize
isSizeNameTest
isSizeNameTestRaw
haveSizedTypes
builtinSizeHook
sizeSort
sizeUniv
sizeType_
sizeType
sizeSucName
sizeSuc
sizeSuc_
sizeMax
data SizeView
sizeView
type Offset
data DeepSizeView
data SizeViewComparable a
sizeViewComparable
sizeViewSuc_
sizeViewPred
sizeViewOffset
removeSucs
unSizeView
unDeepSizeView
type SizeMaxView
maxViewMax
maxViewCons
sizeViewComparableWithMax
maxViewSuc_
unMaxView