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 SizeExpr

data SizeConstraint

computeSizeConstraints

computeSizeConstraint

sizeExpr

flexibleVariables

canonicalizeSizeConstraint

solveSizeConstraints

oldSolver