Nuprl Definition : sm-replica
sm-replica(init;f;Req) ==
smr-class(init;s,cmds.sm-do-ops(s;
s,cmd.
let client,cid,op = cmd in
let s',rsp = f s op
in <s', client, cid, rsp>;cmds);request-buffer(Req))
Proof not projected
Definitions occuring in Statement :
request-buffer: request-buffer(Req),
smr-class: smr-class(init;s,x.F[s; x];X),
sm-do-ops: sm-do-ops(s;f;L),
spreadn: spread3,
apply: f a,
lambda: x.A[x],
spread: spread def,
pair: <a, b>
Definitions :
smr-class: smr-class(init;s,x.F[s; x];X),
sm-do-ops: sm-do-ops(s;f;L),
lambda: x.A[x],
spreadn: spread3,
spread: spread def,
apply: f a,
pair: <a, b>,
request-buffer: request-buffer(Req)
FDL editor aliases :
sm-replica
sm-replica(init;f;Req) ==
smr-class(init;s,cmds.sm-do-ops(s;\mlambda{}s,cmd.
let client,cid,op = cmd in
let s',rsp = f s op
in <s', client, cid, rsp>cmds);request-buffer(Req))
Date html generated:
2011_10_20-PM-04_10_24
Last ObjectModification:
2011_01_25-PM-04_10_04
Home
Index