graph 1 1 Sections Graphs Doc

Def list_accum(x,a.f(x;a);y;l) == Case of l; nil y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive)

is mentioned by

Thm* f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L)[list_accum_filter]
Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1)[filter_list_accum]
Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))[primrec_list_accum]
Thm* l1,l2:Top List, f,y:Top. list_accum(x,a.f(x,a);y;l1 @ l2) ~ list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;l1);l2)[list_accum_append]
Def process u j where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } == if P(j;u) F(j;u) else G(j;list_accum(s',i'.process s' i' where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } ;H(j;u);N(j;u))) fi (recursive)[accumulate]

Try larger context: Graphs

graph 1 1 Sections Graphs Doc