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
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:
2015_07_17-AM-09_10_45
Last ObjectModification:
2012_02_25-AM-10_52_04
Home
Index