list
3
jlc
Sections
Support(jlc)
Doc
Def
filter(f;L) == (letrec filter f L = (Case of L; nil
nil ; h.t
if f(h)
h.filter(f,t) else filter(f,t) fi) ) (f,L)
is mentioned by
Thm*
eq:{T=
}, P:(T
), L:T List, x:T. x(
eq) L
P(x)
x(
eq) filter((
x.P(x));L)
[filter_is_member_lemma]
Thm*
eq:{T=
}, P:(T
), L:T List, x:T. x(
eq) filter((
x.P(x));L)
P(x)
[is_member_filter_lemma]
list
3
jlc
Sections
Support(jlc)
Doc