Step
*
of Lemma
filter-as-accum-aux2
ā[A:Type]. ā[p:A ā¶ š¹]. ā[L:A List]. ā[X:Top List].
(X @ filter(p;L) ~ accumulate (with value a and list item x):
if p[x] then a @ [x] else a fi
over list:
L
with starting value:
X))
BY
{ (Auto
THEN (InstLemma `mapfilter-as-accum-aux` [āAā;āpā;āLā;āXā;āĪ»x.xā]ā
THENA Auto)
THEN (RWO "filter-as-mapfilter<" (-1) THENA Auto)
THEN RWO "-1" 0
THEN RepUR ``so_apply`` 0
THEN Auto) }
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[p:A {}\mrightarrow{} \mBbbB{}]. \mforall{}[L:A List]. \mforall{}[X:Top List].
(X @ filter(p;L) \msim{} accumulate (with value a and list item x):
if p[x] then a @ [x] else a fi
over list:
L
with starting value:
X))
By
Latex:
(Auto
THEN (InstLemma `mapfilter-as-accum-aux` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (RWO "filter-as-mapfilter<" (-1) THENA Auto)
THEN RWO "-1" 0
THEN RepUR ``so\_apply`` 0
THEN Auto)
Home
Index