Nuprl Definition : sm-do-ops
sm-do-ops(s;f;L) == list_accum(p,op.let s,out = p in let s',r = f s op in <s', out @ [r]>;<s, []>;L)
Proof not projected
Definitions occuring in Statement :
append: as @ bs,
apply: f a,
spread: spread def,
pair: <a, b>,
cons: [car / cdr],
nil: [],
list_accum: list_accum(x,a.f[x; a];y;l)
Definitions :
list_accum: list_accum(x,a.f[x; a];y;l),
spread: spread def,
apply: f a,
append: as @ bs,
cons: [car / cdr],
pair: <a, b>,
nil: []
FDL editor aliases :
sm-do-ops
sm-do-ops(s;f;L) ==
list\_accum(p,op.let s,out = p in let s',r = f s op in <s', out @ [r]><s, []>L)
Date html generated:
2011_10_20-PM-04_08_34
Last ObjectModification:
2011_01_24-PM-05_08_19
Home
Index