Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data ErrorNonEmpty
- = Fail
- | FailBecause TCErr
- | DontKnow
- ensureEmptyType :: Range -> Type -> TCM ()
- isEmptyType :: Type -> TCM Bool
- isEmptyTel :: Telescope -> TCM Bool
- checkEmptyType :: Range -> Type -> TCM (Either ErrorNonEmpty ())
- checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
Documentation
data ErrorNonEmpty Source #
Fail | Generic failure |
FailBecause TCErr | Failure with informative error |
DontKnow | Emptyness check blocked |
Instances
Semigroup ErrorNonEmpty Source # | |
Defined in Agda.TypeChecking.Empty (<>) :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty # sconcat :: NonEmpty ErrorNonEmpty -> ErrorNonEmpty # stimes :: Integral b => b -> ErrorNonEmpty -> ErrorNonEmpty # | |
Monoid ErrorNonEmpty Source # | |
Defined in Agda.TypeChecking.Empty mempty :: ErrorNonEmpty # mappend :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty # mconcat :: [ErrorNonEmpty] -> ErrorNonEmpty # |
:: Range | Range of the absurd pattern. |
-> Type | Type that should be empty (empty data type or iterated product of such). |
-> TCM () |
Ensure that a type is empty. This check may be postponed as emptiness constraint.
checkEmptyType :: Range -> Type -> TCM (Either ErrorNonEmpty ()) Source #
checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int) Source #
Check whether one of the types in the given telescope is constructor-less and if yes, return its index in the telescope (0 = leftmost).