Nuprl Definition : disjoint-union-class
X + Y == λb1,b2. if bag-null(b1) then bag-map(λx.(inr x );b2) else bag-map(λx.(inl x);b1) fi |X, Y|
Definitions occuring in Statement :
simple-comb-2: F|X, Y|,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
bag-null: bag-null(bs),
bag-map: bag-map(f;bs)
FDL editor aliases :
disjoint-union-class
Latex:
X + Y == \mlambda{}b1,b2. if bag-null(b1) then bag-map(\mlambda{}x.(inr x );b2) else bag-map(\mlambda{}x.(inl x);b1) fi |X, Y|
Date html generated:
2015_07_22-PM-00_14_20
Last ObjectModification:
2012_11_29-AM-11_15_02
Home
Index