Agda-2.2.8: A dependently typed functional programming language and proof assistant




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

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

data SizeView Source

A useful view on sizes.

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

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

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

Turn a size view into a term.