Nuprl Definition : es-interface-union

X+Y ==  eclass-compose2(λxs,ys. if (#(xs) =z 1) then {inl only(xs)} if (#(ys) =z 1) then {inr only(ys) } else {} fi ;X;Y\000C)


Definitions occuring in Statement :  eclass-compose2: eclass-compose2(f;X;Y),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  lambda: λx.A[x],  inr: inr x ,  inl: inl x,  natural_number: $n,  bag-only: only(bs),  bag-size: #(bs),  single-bag: {x},  empty-bag: {}
FDL editor aliases :  es-interface-union
Latex:
X+Y  ==
    eclass-compose2(\mlambda{}xs,ys.  if  (\#(xs)  =\msubz{}  1)  then  \{inl  only(xs)\}
                                                  if  (\#(ys)  =\msubz{}  1)  then  \{inr  only(ys)  \}
                                                  else  \{\}
                                                  fi  ;X;Y)


Date html generated: 2015_07_20-PM-03_18_56
Last ObjectModification: 2012_02_25-PM-01_40_46

Home Index