is mentioned by
[sfa_doc_ycomb_factorial_typing] | |
[sfa_doc_factbody_polytyping] | |
Thm* (x:. f zero beyond x) & (x:. g zero beyond x) Thm* Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x) | [sfa_doc_alternate_zero_beyond] |
Thm* (n:. f(n) = 0) Thm* Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi) Prop{1} | [sfa_doc_predicativity_sample8] |
Def (recursive) | [sfa_doc_sequence_rel] |
[sfa_doc_max_int] | |
[sfa_doc_ntuple] | |
[sfa_doc_factorial2] | |
[sfa_doc_factorial] | |
[kleene_minimize] |
In prior sections: bool 1 int 2 list 1
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html