Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi
Def (recursive)

is mentioned by

Def R^+(x,y) == n:. x R^n y

[rel_plus]

In prior sections: mb nat mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html