| 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.4.2