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

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 # |
Instance details Defined in Agda.TypeChecking.Empty Methods (<>) :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty Source # sconcat :: NonEmpty ErrorNonEmpty -> ErrorNonEmpty Source # stimes :: Integral b => b -> ErrorNonEmpty -> ErrorNonEmpty Source #
Monoid ErrorNonEmpty Source # |
Instance details Defined in Agda.TypeChecking.Empty Methods mempty :: ErrorNonEmpty Source # mappend :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty Source # mconcat :: [ErrorNonEmpty] -> ErrorNonEmpty Source #

ensureEmptyType Source #

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).