Selected Objects

COM	rfunction_com2	The '{f | x:A  B}' type is the type of functions with domain 'A' and range type 'B(f,x)' on argument 'x', where 'f' is the function itself. ...
def	fincr	FIncr == {f | i:  if i=0  else {f(i-1)...} fi}
COM	fincr_wf_com	Note that is this case, we use a supertype of the range to prove that 'FIncr' is well formed. Then, in the prove of wf, we show that 'f' with a restricted domain lies in the type ''. Afterwards, we use the fact that 'f(i)  ' for an unrestricted range. We are duplicating work.
THM	fincr_formation	FIncr

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