Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Empty
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 #
Constructors
Fail | Generic failure |
FailBecause TCErr | Failure with informative error |
DontKnow | Emptyness check blocked |
Instances
Semigroup ErrorNonEmpty Source # | |
Defined in Agda.TypeChecking.Empty Methods (<>) :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty sconcat :: NonEmpty ErrorNonEmpty -> ErrorNonEmpty stimes :: Integral b => b -> ErrorNonEmpty -> ErrorNonEmpty | |
Monoid ErrorNonEmpty Source # | |
Defined in Agda.TypeChecking.Empty Methods mappend :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty mconcat :: [ErrorNonEmpty] -> ErrorNonEmpty |
Arguments
:: 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.
isEmptyType :: Type -> TCM Bool Source #
Check whether a type is empty.
isEmptyTel :: Telescope -> TCM Bool Source #
Check whether some type in a telescope is empty.
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).