Nuprl - rfunction com2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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.
That is, this is a type of highly dependent functions, whose range type depends on calls to the function itself. In this version, the domain type 'A' must be well-founded with some relation 'R' , and the calls to the function in the range 'B' must always obey 'R'.
Here is a formal description of the type, along with its members.
We define '{f | x:A

B}' to be a type with membership 'phi' iff there is an 'alpha' such that

1. 'A' is a type with membership 'alpha'
2. 'A' is well-founded with respect to some partial order'R'
3. for any'a' such that'alpha(a)'
there is a'gamma_?' such that
for all'b R a',
a.'{f | x:{c:A| c R b } B}' is a type with membership'gamma_b',
b. there is a'beta_?' such that
i. for any'g' such that'gamma_b(g)',
'B(g,b)' is a type with membership'beta_g'
ii. for any'f','phi(f)' iff
for all'a' such that'alpha(a)','beta_a(f(a))'

About:

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

rfunction 1 Sections StandardLIB Doc