Nuprl Definition : disjoint-union-tr
tr1 + tr2 == λl,a,s. if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi
Definitions occuring in Statement :
outr: outr(x),
outl: outl(x),
ifthenelse: if b then t else f fi ,
isl: isl(x),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
disjoint-union-tr
Latex:
tr1 + tr2 == \mlambda{}l,a,s. if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi
Date html generated:
2015_07_22-PM-00_07_20
Last ObjectModification:
2012_11_29-AM-11_13_27
Home
Index