Nuprl Definition : ml-filter
ml-filter(P;L) ==
fix((λfilter,P,L. if null(L) then [] else let x.y = L in if P(x) then [x / filter(P)(y)] else filter(P)(y) fi fi ))(P\000C)(L)
Definitions occuring in Statement :
spreadcons: spreadcons,
ml_apply: f(x),
null: null(as),
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
fix: fix(F),
lambda: λx.A[x]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
null: null(as),
nil: [],
spreadcons: spreadcons,
ifthenelse: if b then t else f fi ,
cons: [a / b],
ml_apply: f(x)
FDL editor aliases :
ml-filter
Latex:
ml-filter(P;L) ==
fix((\mlambda{}filter,P,L. if null(L)
then []
else let x.y = L
in if P(x) then [x / filter(P)(y)] else filter(P)(y) fi
fi ))(P)(L)
Date html generated:
2017_09_29-PM-05_50_57
Last ObjectModification:
2017_05_19-PM-02_11_28
Theory : ML
Home
Index