WhoCites Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites fincr?
fincrDef FIncr == {f | i:  if i=0  else {f(i-1)...} fi}
Thm* FIncr  Type
Thm* FIncr  Type
int_upperDef {i...} == {j:ij }
Thm* n:. {n...}  Type
eq_intDef i=j == if i=j true ; false fi
Thm* i,j:. (i=j 
natDef  == {i:| 0i }
Thm*   Type
leDef AB == B<A
Thm* i,j:. (ij Prop
notDef A == A  False
Thm* A:Prop. (A Prop

Syntax:FIncr has structure: fincr

About:
boolbfalsebtrueifthenelseintnatural_numbersubtractint_eqless_than
setapplyuniversememberpropimpliesfalseall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions StandardLib Sections NuprlLIB Doc