Step
*
of Lemma
mapfilter-as-accum
ā[A:Type]. ā[L:A List]. ā[p:A ā¶ š¹]. ā[f:Top].
(mapfilter(f;p;L) ~ accumulate (with value a and list item x):
if p[x] then a @ [f[x]] else a fi
over list:
L
with starting value:
[]))
BY
{ (Auto THEN (InstLemma `mapfilter-as-accum-aux` [āAā;āpā;āLā;ā[]ā;āfā]ā
THENA Auto) THEN Reduce (-1) THEN Auto) }
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[L:A List]. \mforall{}[p:A {}\mrightarrow{} \mBbbB{}]. \mforall{}[f:Top].
(mapfilter(f;p;L) \msim{} accumulate (with value a and list item x):
if p[x] then a @ [f[x]] else a fi
over list:
L
with starting value:
[]))
By
Latex:
(Auto
THEN (InstLemma `mapfilter-as-accum-aux` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Reduce (-1)
THEN Auto)
Home
Index