Def b == if b True else False fi

is mentioned by

Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))	[mu-property]
Thm* f:(). (n:. f(n))  mu(f)	[mu_wf]

In prior sections: bool 1 list 1 union mb nat mb list 1 mb list 2 rel 1

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