Nuprl Definition : ohc_v1_when

Nuprl Definition : ohc_v1_when_quorum1

ohc_v1_when_quorum1(Cmd;cmdeq;flrs) ==

ni,loc,vt,state.if ohc_v1_newvote() ni vt state then ohc_v1_roundout1(Cmd;cmdeq;flrs) loc vt state else {} fi

Definitions occuring in Statement : ohc_v1_roundout1: ohc_v1_roundout1(Cmd;cmdeq;flrs), ohc_v1_newvote: ohc_v1_newvote(), ifthenelse: if b then t else f fi , apply: f a, lambda:

x.A[x], empty-bag: {}
FDL editor aliases : ohc_v1_when_quorum1 ohc_v1_when_quorum1

ohc\_v1\_when\_quorum1(Cmd;cmdeq;flrs) == \mlambda{}ni,loc,vt,state. if ohc\_v1\_newvote() ni vt state then ohc\_v1\_roundout1(Cmd;cmdeq;flrs) loc vt state else \{\} fi Date html generated: 2012_02_20-PM-05_21_34 Last ObjectModification: 2012_02_13-PM-12_55_33 Home Index