Nuprl Definition : bag-splits

bag-splits(b) ==  rec-case(b) of [] => {<{}, {}>a::as => r.bag-map(λp.<{a} (fst(p)), snd(p)>;r) bag-map(λp.<fst(\000Cp), {a} (snd(p))>;r)



Definitions occuring in Statement :  bag-append: as bs bag-map: bag-map(f;bs) single-bag: {x} empty-bag: {} list_ind: list_ind pi1: fst(t) pi2: snd(t) lambda: λx.A[x] pair: <a, b>
Definitions occuring in definition :  list_ind: list_ind empty-bag: {} bag-map: bag-map(f;bs) lambda: λx.A[x] pair: <a, b> pi1: fst(t) bag-append: as bs single-bag: {x} pi2: snd(t)
FDL editor aliases :  bag-splits

Latex:
bag-splits(b)  ==
    rec-case(b)  of
    []  =>  \{<\{\},  \{\}>\}
    a::as  =>
      r.bag-map(\mlambda{}p.<\{a\}  +  (fst(p)),  snd(p)>r)  +  bag-map(\mlambda{}p.<fst(p),  \{a\}  +  (snd(p))>r)



Date html generated: 2016_05_15-PM-02_52_45
Last ObjectModification: 2015_09_23-AM-07_40_31

Theory : bags


Home Index