Def  i<j == if i<j true ; false fi

is mentioned by

Def  Iter(f;u) i:{a..b}. e(i) Def  == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi Def  (recursive)

[iter_via_intseg]

In prior sections: bool 1

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