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

Safe Haskell | Safe-Infered

Agda.TypeChecking.Monad.SizedTypes

Synopsis

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

# Documentation

isSizeType :: Type -> TCM Bool

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

isSizeNameTest :: TCM (QName -> Bool)

isSizeTypeTest :: TCM (Type -> Bool)

sizeType :: TCM Type

sizeSuc :: TCM (Maybe QName)

data SizeView

A useful view on sizes.

Constructors

SizeInf |
SizeSuc Term |
OtherSize Term |

sizeView :: Term -> TCM SizeView

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

unSizeView :: SizeView -> TCM Term

Turn a size view into a term.