Agda.TypeChecking.SizedTypes

SIZELT stuff

checkSizeLtSat

checkSizeNeverZero

checkSizeVarNeverZero

isBounded

boundedSizeMetaHook

trySizeUniv

Size views that reduce.

deepSizeView

sizeMaxView

Size comparison that might add constraints.

compareSizes

compareMaxViews

compareBelowMax

compareSizeViews

trivial

Size constraints.

isSizeProblem

isSizeConstraint

getSizeConstraints

getSizeMetas

Size constraint solving.

data OldSizeExpr

data OldSizeConstraint

oldComputeSizeConstraints

oldComputeSizeConstraint

oldSizeExpr

flexibleVariables

oldCanonicalizeSizeConstraint

oldSolveSizeConstraints

oldSolver