Data.Singletons.Types

Defines and exports types that are useful when working with singletons. Some of these are re-exports from Data.Type.Equality.

Documentation

type Refuted a = a -> Void

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

data Decision a

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a

Witness for a

Disproved (Refuted a)

Proof that no a exists