Nuprl Definition : rsc5_update

Nuprl Definition : rsc5_update_replica

rsc5_update_replica(Cmd) ==

zl.let n,c = zl
in

z.let max,missing = z
            in if max <z n then <n, missing @ [max + 1, n)>
               if deq-member(IntDeq;n;missing) then <max, list-diff(IntDeq;missing;[n])>
               else <max, missing>
               fi

Definitions occuring in Statement : append: as @ bs, lt_int: i <z j, ifthenelse: if b then t else f fi , lambda:

x.A[x], spread: spread def, pair: <a, b>, cons: [car / cdr], nil: [], add: n + m, natural_number: $n, list-diff: list-diff(eq;as;bs), deq-member: deq-member(eq;x;L), int-deq: IntDeq, from-upto: [n, m)
FDL editor aliases : rsc5_update_replica

rsc5\_update\_replica(Cmd) == \mlambda{}zl.let n,c = zl in \mlambda{}z.let max,missing = z in if max <z n then <n, missing @ [max + 1, n)> if deq-member(IntDeq;n;missing) then <max, list-diff(IntDeq;missing;[n])> else <max, missing> fi Date html generated: 2012_02_20-PM-05_08_58 Last ObjectModification: 2012_02_02-PM-02_19_34 Home Index