Void

There are also other ways to express the empty type by means of other Nuprl primitives, such as,

Thm* Void =ext {x:| x<x }

Thm* Void =ext rec(A.A)

Thm* Void =ext (x:. {x:}) since these singleton types are disjoint.

And of course, Thm* Void  A.

Here are a few examples of how Void relates to other type constructors.

Thm* VoidA =ext Void

Thm* Void List =ext {nil:Void List}

Thm* VoidA =ext {x.x:VoidA}

The last theorem above states that VoidA has only the one member (x.x). This is a degenerate function in that it cannot be applied to anything in Void. Indeed, the body of the function expression is irrelevant since it will never be evaluated as part of application to any argument of type Void.

Thm* (x.whatever) = (x.x)  VoidA

So, although VoidA has only one member, every (closed) lambda expression denotes that member. See Functions.

Similarly, the intersection over the empty domain is a trivial one-element type whose single member is denoted by every expression that can denote at all:

Thm* whatever1 = whatever2  Whatever(given Void)

Thm* whatever1 = whatever2  (x:Void. Whatever(x))

Sometimes this last type is denoted "Top" since:

Thm* A  Top

where Def Top == Void(given Void).

See Polymorphism.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html