Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Monad.SizedTypes

Synopsis

isSizeType :: MonadTCM tcm => Type -> tcm Bool sizeType :: MonadTCM tcm => tcm Type sizeSuc :: MonadTCM tcm => tcm (Maybe QName) data SizeView = SizeInf | SizeSuc Term | OtherSize Term sizeView :: MonadTCM tcm => Term -> tcm SizeView unSizeView :: MonadTCM tcm => SizeView -> tcm Term

Documentation

isSizeType :: MonadTCM tcm => Type -> tcm Bool Source

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

sizeType :: MonadTCM tcm => tcm Type Source

sizeSuc :: MonadTCM tcm => tcm (Maybe QName) Source

data SizeView Source

A useful view on sizes. Constructors SizeInf SizeSuc Term OtherSize Term

sizeView :: MonadTCM tcm => Term -> tcm SizeView Source

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

unSizeView :: MonadTCM tcm => SizeView -> tcm Term Source

Turn a size view into a term.

Produced by Haddock version 2.6.0