Nuprl Definition : lg-filter
lg-filter(P;G) == let rms = filter(λi.(¬b(P (fst(G[i]))));upto(lg-size(G))) in reduce(λx,g. lg-remove(g;x);G;rms)
Definitions occuring in Statement :
lg-remove: lg-remove(g;n),
lg-size: lg-size(g),
upto: upto(n),
filter: filter(P;l),
select: L[n],
reduce: reduce(f;k;as),
bnot: ¬bb,
let: let,
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
lg-filter
Latex:
lg-filter(P;G) ==
let rms = filter(\mlambda{}i.(\mneg{}\msubb{}(P (fst(G[i]))));upto(lg-size(G))) in
reduce(\mlambda{}x,g. lg-remove(g;x);G;rms)
Date html generated:
2015_07_22-PM-00_28_32
Last ObjectModification:
2012_02_25-PM-03_34_22
Home
Index