Nuprl Definition : bag-decomp
bag-decomp(bs) == map(λn.remove-nth(n;bs);upto(||bs||))
Definitions occuring in Statement :
upto: upto(n),
remove-nth: remove-nth(n;L),
length: ||as||,
map: map(f;as),
lambda: λx.A[x]
Definitions occuring in definition :
map: map(f;as),
lambda: λx.A[x],
remove-nth: remove-nth(n;L),
upto: upto(n),
length: ||as||
FDL editor aliases :
bag-decomp
Latex:
bag-decomp(bs) == map(\mlambda{}n.remove-nth(n;bs);upto(||bs||))
Date html generated:
2016_05_15-PM-02_54_00
Last ObjectModification:
2015_09_23-AM-07_40_35
Theory : bags
Home
Index