Def b == if b True else False fi

is mentioned by

Thm* L:T List, P:(TT). Thm* (x,y:T. P(x,y)  P(y,x)) Thm*  Thm* (L':T List.  Thm* ((L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L') Thm* (& (i:(||L'||-1). P(L'[i],L'[(i+1)])))	[partial_sort_exists_2]
Thm* P:(L:(T List)(||L||-1)), m:((T List)). Thm* (L:T List, i:(||L||-1). Thm* (P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)) Thm*  Thm* (L:T List.  Thm* (L':T List.  Thm* ((L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))	[partial_sort_exists]
Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'. Thm* (x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))	[member_map_filter]
Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List. Thm* mapfilter(f;P;L)  T' List	[mapfilter_wf]
Thm* l:T List, P:(T), x,y:T. Thm* x before y  filter(P;l)  P(x) & P(y) & x before y  l	[l_before_filter]
Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))	[sublist_filter]
Thm* L:T List, P:(T). (xL.P(x))  reduce(x,y. P(x)y;true;L)	[l_all_reduce]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ nil)	[filter_is_nil]
Thm* P:(T), L:T List. (xL.P(x))  filter(P;L) = L	[filter_trivial2]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ L)	[filter_trivial]

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

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