Agda-2.6.0: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Empty
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.
ensureEmptyType Source #
Arguments
Range of the absurd pattern.
Type that should be empty (empty data type or iterated product of such).
Ensure that a type is empty. This check may be postponed as emptiness constraint.