Nuprl Definition : OARcast_on_order_output
OARcast_on_order_output(M) ==
λslf,z,state. let sndr,z = z in let n,msg = z in if sndr ∈b state) then {} else {sndr} fi
Definitions occuring in Statement :
id-deq: IdDeq,
deq-member: x ∈b L),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
spread: spread def,
single-bag: {x},
empty-bag: {}
FDL editor aliases :
OARcast_on_order_output
Latex:
OARcast\_on\_order\_output(M) ==
\mlambda{}slf,z,state. let sndr,z = z in let n,msg = z in if sndr \mmember{}\msubb{} state) then \{\} else \{sndr\} fi
Date html generated:
2015_07_23-PM-00_32_02
Last ObjectModification:
2014_08_20-PM-00_04_41
Home
Index