Agda.TypeChecking.Monad.SizedTypes

Documentation

isSizeType :: MonadTCM tcm => Type -> tcm Bool

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

sizeType :: MonadTCM tcm => tcm Type

sizeSuc :: MonadTCM tcm => tcm (Maybe QName)

data SizeView

A useful view on sizes.

Constructors

SizeInf

SizeSuc Term

OtherSize Term

sizeView :: MonadTCM tcm => Term -> tcm SizeView

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

unSizeView :: MonadTCM tcm => SizeView -> tcm Term

Turn a size view into a term.