Documentation
isSizeType :: MonadTCM tcm => Type -> tcm BoolSource
Check if a type is the primSize
type. The argument should be reduce
d.
sizeView :: MonadTCM tcm => Term -> tcm SizeViewSource
Compute the size view of a term. The argument should be reduce
d.
Precondition: sized types are enabled.
unSizeView :: MonadTCM tcm => SizeView -> tcm TermSource
Turn a size view into a term.