Nuprl Definition : pv11_p1_p2a'broadcast

pv11_p1_p2a'broadcast(Cmd;mf) ==  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``pv11_p1 p2a``;z));locs)



Definitions occuring in Statement :  mk-msg-interface: mk-msg-interface(l;m) make-Msg: make-Msg(hdr;val) cons: [a b] nil: [] lambda: λx.A[x] token: "$token" bag-map: bag-map(f;bs)
FDL editor aliases :  pv11_p1_p2a'broadcast

Latex:
pv11\_p1\_p2a'broadcast(Cmd;mf)  ==
    \mlambda{}locs,z.  bag-map(\mlambda{}l.mk-msg-interface(l;make-Msg(``pv11\_p1  p2a``;z));locs)



Date html generated: 2015_07_23-PM-04_12_06
Last ObjectModification: 2014_11_26-AM-11_23_48

Home Index