Def mu(f) == if f(0) 0 else 1+mu(x.f(1+x)) fi  (recursive)

This unbounded search function was first typed by a proof presented in a Nuprl seminar in 1984 by sfa as part of an argument that the so-called direct computation rules should be included in the Nuprl system. These rules allow type-free rewrites according how terms compute (see Computation). The rules for direct computation were adopted and are described in the Nuprl book of 1986. These rules depended only on the fact that Kleene-equality preserved identity over any type, and did not allow rewriting arbitrary subterms. Later Doug Howe proved that, indeed, rewriting arbitrary subterms would also preserve equality over any type given a few natural constraints on computation and type definition.

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