Agda.TypeChecking.SizedTypes.Solve

type CC

data DefaultToInfty

solveSizeConstraints

castConstraintToCurrentContext'

castConstraintToCurrentContext

solveSizeConstraints_

solveCluster

getSizeHypotheses

canonicalizeSizeConstraint

data NamedRigid

data SizeMeta

type DBSizeExpr

type SizeConstraint

data HypSizeConstraint

computeSizeConstraint

sizeExpr

unSizeExpr