Agda.TypeChecking.SizedTypes

builtinSizeHook

deepSizeView

sizeMaxView

trySizeUniv

compareSizes

compareMaxViews

compareBelowMax

compareSizeViews

isBounded

trivial

boundedSizeMetaHook

isSizeProblem

isSizeConstraint

getSizeConstraints

getSizeMetas

data SizeExpr

data SizeConstraint

computeSizeConstraints

computeSizeConstraint

sizeExpr

flexibleVariables

haveSizedTypes

canonicalizeSizeConstraint

solveSizeConstraints