Nuprl Definition : PV2_test1
PV2_test1() ==
accpts,ldrs,ldrs_uid,reps.
(TERMOF{PV2_paxos_main_programmable:o, 1:l, 1:l} 
accpts (op,state.let k = op + state in <k, k>) IntDeq IntDe\000Cq 0 ldrs
ldrs_uid
reps)
Definitions occuring in Statement :
let: let,
apply: f a,
lambda: x.A[x],
pair: <a, b>,
add: n + m,
natural_number: $n,
int: ,
int-deq: IntDeq
FDL editor aliases :
PV2_test1
PV2\_test1() ==
\mlambda{}accpts,ldrs,ldrs$_{uid}$,reps.
(TERMOF\{PV2\_paxos\_main\_programmable:o, 1:l, 1:l\} \mBbbZ{} \mBbbZ{} \mBbbZ{} \mBbbZ{} accpts
(\mlambda{}op,state.let k = op + state in <k, k>)
IntDeq
IntDeq
0
ldrs
ldrs$_{uid}$
reps)
Date html generated:
2012_02_20-PM-07_13_27
Last ObjectModification:
2012_02_02-PM-03_08_41
Home
Index