Safe Haskell | Safe-Infered |
---|
Agda.TypeChecking.Monad.SizedTypes
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)
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.