ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Empty

Synopsis

valueisEmptyType :: MonadTCM tcm => Type -> tcm Bool

Check whether a type is empty.

valueisEmptyTel :: MonadTCM tcm => Telescope -> tcm Bool

Check whether some type in a telescope is empty.

valueensureEmptyType

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

valuecheckEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)

Check whether one of the types in the given telescope is constructor-less and if yes, return its index in the telescope (0 = leftmost).