Nuprl Definition : OARcast_deliverer_for_sender_update
OARcast_deliverer_for_sender_update(M) ==
λsndr,slf,z,state. let orderer,z = z
in let sndr,z = z
in let seq,m = z
in if seq ∈b state) then state else [seq / state] fi
Definitions occuring in Statement :
deq-member: x ∈b L)
,
int-deq: IntDeq
,
cons: [a / b]
,
ifthenelse: if b then t else f fi
,
lambda: λx.A[x]
,
spread: spread def
FDL editor aliases :
OARcast_deliverer_for_sender_update
Latex:
OARcast\_deliverer\_for\_sender\_update(M) ==
\mlambda{}sndr,slf,z,state. let orderer,z = z
in let sndr,z = z
in let seq,m = z
in if seq \mmember{}\msubb{} state) then state else [seq / state] fi
Date html generated:
2015_07_23-PM-00_33_55
Last ObjectModification:
2014_08_20-PM-00_07_11
Home
Index