Nuprl Definition : Paxos-spec8-spec75
NoProposal == λtr.let b,b',v = tr in if b ≤z b' then inl b else inr ⋅ fi [Collect1]
Definitions occuring in Statement :
abbreviation: Collect1,
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
it: ⋅,
spreadn: spread3,
lambda: λx.A[x],
inr: inr x ,
inl: inl x
NoProposal == \mlambda{}tr.let b,b',v = tr in if b \mleq{}z b' then inl b else inr \mcdot{} fi [Collect1]
Date html generated:
2015_07_17-AM-09_10_46
Last ObjectModification:
2012_02_25-AM-10_52_04
Home
Index