Def  if b t else f fi == InjCase(b; . t, f)

is mentioned by

Thm*  (A+B) ~ (i:2if i=0 A else B fi)	[card_union_vs_sigma]
Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)	[union_sigma_inverses]
Thm*  A,B:Type. sigma_to_union  (i:2if i=0 A else B fi)(A+B)	[sigma_to_union_wf]
Thm*  A,B:Type. union_to_sigma  (A+B)(i:2if i=0 A else B fi)	[union_to_sigma_wf]
Thm*  Dec(P)  (!i:2. if i=0 P else P fi)	[decidable_vs_unique_nsub2]
Thm*  {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype_ooc]
Thm*  a:, b:, j:b, f:((a-1) inj {x:b| x = j }). Thm*  (i.if i=a-1 j else f(i) fi)  a inj b	[nsub_inj_fill_typing]
Def  size(a)(p) == Msize(x.if p(x) 1 else 0 fi)	[boolsize]
Def  prev_nat_pair(xy) == xy/x,y. if x=0 <y-1,0> else <x-1,y+1> fi	[prev_nat_pair]
Def  next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else <x+1,y-1> fi	[next_nat_pair]
Def  [x/ xs](i) == if i=0 x else xs(i-1) fi	[seq_cons]
Def  sigma_to_union(e) == e/i,u. if i=0 inl(u) else inr(u) fi	[sigma_to_union]
Def  find_first_iter(v.p(v); v.f(v); a) Def  == if p(a) a else find_first_iter(v.p(v); v.f(v); f(a)) fi Def  (recursive)	[find_first_iter]
Def  least i:. p(i) == if p(0) 0 else (least i:. p(i+1))+1 fi  (recursive)	[least]
Def  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)	[compose_iter]
Def  (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi	[replace_fn_values]

In prior sections: bool 1 LogicSupplement int 2 num thy 1 IteratedBinops

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