Nuprl Definition : s-filter
s-filter(p;as) ==  reduce(λa,l. if p a then s-insert(a;l) else l fi [];as)
Definitions occuring in Statement : 
s-insert: s-insert(x;l), 
reduce: reduce(f;k;as), 
nil: [], 
ifthenelse: if b then t else f fi , 
apply: f a, 
lambda: λx.A[x]
Definitions occuring in definition : 
reduce: reduce(f;k;as), 
lambda: λx.A[x], 
ifthenelse: if b then t else f fi , 
apply: f a, 
s-insert: s-insert(x;l), 
nil: []
FDL editor aliases : 
s-filter
Latex:
s-filter(p;as)  ==    reduce(\mlambda{}a,l.  if  p  a  then  s-insert(a;l)  else  l  fi  ;[];as)
Date html generated:
2016_05_15-PM-03_52_10
Last ObjectModification:
2015_09_23-AM-07_45_16
Theory : general
Home
Index