Module Preface_core.VoidSource

Void describes unhabited type. A type that is not representable.

Sourcetype t

Expressing a value of this type is impossible.

Sourceval absurd : t -> 'a

The law according to which any statement can be proven from a contradiction. That is, once a contradiction has been asserted, any proposition (including their negations) can be inferred from it; this is known as deductive explosion.

As an identity for Either

Void.t act as an identity for Either.

Sourceval left : ('a, t) Either.t -> 'a

If there is void on the right part of Either, we know that the Either is in Left branch.

Sourceval right : (t, 'b) Either.t -> 'b

If there is void on the left part of Either, we know that the Either is in Right branch.