Nuprl Definition : OARcast_SenderState
OARcast_SenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==
state-class1(λslf.0;OARcast_on_oarcast_update(M);OARcast_oarcast'base(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
Definitions occuring in Statement :
OARcast_on_oarcast_update: OARcast_on_oarcast_update(M)
,
OARcast_oarcast'base: OARcast_oarcast'base(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
,
state-class1: state-class1(init;tr;X)
,
lambda: λx.A[x]
,
natural_number: $n
FDL editor aliases :
OARcast_SenderState
Latex:
OARcast\_SenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==
state-class1(\mlambda{}slf.0;OARcast\_on\_oarcast\_update(M);OARcast\_oarcast'base(M;...;...;...;orderhdr;mf))
Date html generated:
2015_07_23-PM-00_30_19
Last ObjectModification:
2014_08_20-PM-00_01_48
Home
Index