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

Safe HaskellSafe-Infered

Agda.TypeChecking.Monad.SizedTypes

Synopsis

Documentation

isSizeType :: Type -> TCM Bool

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

data SizeView

A useful view on sizes.

sizeView :: Term -> TCM SizeView

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

unSizeView :: SizeView -> TCM Term

Turn a size view into a term.