Module Prime

A type which is uninhabited by well-founded code. This is equivalent to a variant type with no constructors, though syntax forbids naming or defining such types.

Computations in the scope of a variable x : counit can be assumed dead, and thus be shortcut as absurd x. This is the analogue of pattern-matching a variant with no constructors.

The I combinator: ident x is x.

The K combinator: konst x y is x.

Function composition: (g % f) x is g (f x).

Reversed function composition: (f %> g) x is g (f x).

curry f x y is f (x, y).

uncurry f (x, y) is f x y.