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

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

Check if a type is the `primSize` type. The argument should be `reduce`d.

sizeType :: MonadTCM tcm => tcm Type

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

data SizeView

A useful view on sizes.

Constructors

SizeInf |
SizeSuc Term |
OtherSize Term |

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

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

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

Turn a size view into a term.