The transfinite W--type of well--founded
trees, 
, used to represent
Brouwer ordinals is inexpressible
in the Nuprl
logic discussed in the earlier chapters
but can be represented in the logic extended by rec types as
rec(w. x:A#(B->w)).
The data type for programs given in chapter 11,
d:N#ind(d; x,y.void; void; x,T. Atomic_Stmt | (T#T) |
(expr#T) | expr#T#T),
can be written more elegantly as
rec(T. Atomic_Stmt | (T#T) | (expr#T) | expr#T#T).The list type constructor is now redundant because A list can be expressed as rec(l. NIL | A#l).