Definitions
MarkB
generic
Sections
NuprlLIB
Doc
No other cites to report in MarkB_generic
list_accum
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)
Thm*
T,T':Type, l:T List, y:T', f:(T'
T
T'). list_accum(x,a.f(x,a);y;l)
T'
Syntax:
list_accum(x,a.f(x;a);y;l)
has structure:
list_accum(x,a.f(x;a); y; l)
About:
Definitions
MarkB
generic
Sections
NuprlLIB
Doc