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:
2016_05_17-PM-02_49_20
Last ObjectModification:
2014_11_26-AM-11_23_48
Theory : paxos!synod
Home
Index