Nuprl Definition : Paxos-spec8-spec74
Proposal == λtr.let b,b',v = tr in if b' <z b then inl <b, v> else inr ⋅ fi [Collect1]
Definitions occuring in Statement :
abbreviation: Collect1,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
it: ⋅,
spreadn: spread3,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
inl: inl x
Latex:
Proposal == \mlambda{}tr.let b,b',v = tr in if b' <z b then inl <b, v> else inr \mcdot{} fi [Collect1]
Date html generated:
2016_05_16-AM-10_53_03
Last ObjectModification:
2012_02_25-AM-10_52_04
Theory : event-ordering
Home
Index