(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ycomb factorial typing
  Y(f,x. if x=0 1 else xf(x-1) fi)  
By: FunExtensionality

Generated subgoals:

1   Y(f,x. if x=0 1 else xf(x-1) fi)  VoidVoid
1 step
2 1. x : 
  Y((f,x. if x=0 1 else xf(x-1) fi),x)  
6 steps

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

(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc