Def  == {i:| 0i }

is mentioned by

Thm* Y(f,x. if x=0 1 else xf(x-1) fi)	[sfa_doc_ycomb_factorial_typing]
Thm* (f,x. if x=0 1 else xf(x-1) fi)  (k:. (k)(k+1))	[sfa_doc_factbody_polytyping]
Thm* (x.x) = (x.if x<0 0 ; x fi)	[sfa_doc_funeq_example1]
Thm* (n.n<0) = (n.false)	[sfa_doc_sqtype_ctr_example_part2]
Thm* x:. y:. yyx & x<(y+1)(y+1)	[sfa_doc_nat_sqrt]
Thm* A:Type, a:A, e:(AA), i:. i steps of e from a  A	[sfa_doc_sequence_rel_wf]
Thm* (x.Case of x Thm* (x.Canil  0 Thm* (x.Cau.v, rec:r  InjCase(if u<r inl(*) ; inr(.*) fi; a. r; b. u+1)) Thm* = Thm* ext{sfa_doc_find_small_greater_bound} Thm*  (k:. x:(k List){y:(k+1)| y greater-bounds x })	[sfa_doc_find_small_greater_bound_extr_eq]
Thm* (k,x. k) Thm* = Thm* ext{sfa_doc_find_greater_bound_stupidly} Thm*  k:x:(k List){y:(k+1)| y greater-bounds x }	[sfa_doc_find_greater_bound_stupidly_extr_eq]
Thm* k:x:(k List){y:(k+1)| y greater-bounds x }	[sfa_doc_find_greater_bound_stupidly]
Thm* k:. x:(k List){y:(k+1)| y greater-bounds x }	[sfa_doc_find_small_greater_bound]
Thm* f,g:(). 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* a,b:. max(a;b)	[sfa_doc_max_int_wf]
Thm* x:, f:(). f zero beyond x  Prop	[sfa_doc_props_as_types_example1_wf]
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))	[sfa_doc_or_dec]
Thm* f:().  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]
Thm* A:Type, P:(AProp), n:, X:(A^n). ( u in X: A^n. P(u))  Prop	[sfa_doc_ntuple_contains_wf]
Thm* n:. n2  (A^n) = A(A^(n-1))	[sfa_doc_ntuple_is_prod]
Thm* A:Type, n:. (A^n)  Type	[sfa_doc_ntuple_wf]
Thm* x:{x:| (x rem 2) = 0 }. x!	[sfa_doc_factorial2_wf]
Thm* x:. x!	[sfa_doc_factorial_wf]
Thm* k:. 0<k & (2  k)<1  2<k	[sfa_doc_cand_example]
Thm* f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)	[kleene_minimize_is_lb]
Thm* f:{f:()| x:. f(x) }. f(mu(f))	[kleene_minimize_is_fp]
Thm* mu  {f:()| x:. f(x) }	[kleene_minimize_wf]
Thm* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) }	[kleene_tail]
Def f zero beyond x == y:. x<y  f(y) = 0	[sfa_doc_props_as_types_example1]
Def sfa_doc_oparm_sample{2:n}(A) == A	[sfa_doc_oparm_sample2]
Def sfa_doc_oparm_sample{1:n}(A) == A	[sfa_doc_oparm_sample1]
Def Induction for x:. P(x) == P(0) & (x:. P(x)  P(x+1))  (x:. P(x))	[sfa_doc_indscheme]
Def  u in X: A^n. P(u) Def == n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u))) Def (recursive)	[sfa_doc_ntuple_contains]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1

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