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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Empty

Synopsis

Documentation

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

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.