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

Thu Sep 14 08:45:18 EDT 1995