Agda.TypeChecking.Empty

Documentation

isEmptyType

Arguments

:: Range

Range of the absurd pattern.

-> Type

Type that should be empty (empty data type or iterated product of such).

-> TCM ()

Check whether a type is empty. This check may be postponed as emptiness constraint.