Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 BoolSource
Check if a type is the primSize type. The argument should be reduced.
sizeType :: MonadTCM tcm => tcm TypeSource
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 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.
Produced by Haddock version 2.4.2