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

Agda.TypeChecking.Monad.SizedTypes

Synopsis

Documentation

isSizeType :: 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 :: Term -> TCM SizeViewSource

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

unSizeView :: SizeView -> TCM TermSource

Turn a size view into a term.