Agda.TypeChecking.Empty

Documentation

isEmptyType :: Type -> TCM Bool

Check whether a type is empty.

isEmptyTel :: Telescope -> TCM Bool

Check whether some type in a telescope is empty.

ensureEmptyType

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.

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