Documentation
isSizeType :: Type -> TCM BoolSource
Check if a type is the primSize
type. The argument should be reduce
d.
isSizeNameTest :: TCM (QName -> Bool)Source
isSizeTypeTest :: TCM (Type -> Bool)Source
sizeView :: Term -> TCM SizeViewSource
Compute the size view of a term. The argument should be reduce
d.
Precondition: sized types are enabled.
unSizeView :: SizeView -> TCM TermSource
Turn a size view into a term.