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

is mentioned by

Def  complete_intseg_mset(a; b; f)(x) == if a  x < b f(x) else 0 fi	[complete_intseg_mset]
Def  split_factor1(g; x)(u) Def  == if u=x g(x)+g(xx)+g(xx) ; u=xx 0 else g(u) fi	[split_factor1]
Def  split_factor2(g; x; y)(u) Def  == if u=x g(x)+g(xy) ; u=y g(y)+g(xy) ; u=xy 0 else g(u) fi	[split_factor2]
Def  reduce_factorization(f; j)(i) == if i=j f(i)-1 else f(i) fi	[reduce_factorization]
Def  trivial_factorization(z)(i) == if i=z 1 else 0 fi	[trivial_factorization]
Def  prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi	[prime_mset_complete]

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