Agda.TypeChecking.Monad.SizedTypes

Documentation

isSizeType :: Type -> TCM Bool

Check if a type is the primSize type. The argument should be reduced.

isSizeNameTest :: TCM (QName -> Bool)

isSizeTypeTest :: TCM (Type -> Bool)

sizeType :: TCM Type

sizeSuc :: TCM (Maybe QName)

data SizeView

A useful view on sizes.

Constructors

SizeInf

SizeSuc Term

OtherSize Term

sizeView :: Term -> TCM SizeView

Compute the size view of a term. The argument should be reduced. Precondition: sized types are enabled.

unSizeView :: SizeView -> TCM Term

Turn a size view into a term.