Nuprl Definition : collect_filter
collect_filter() == λs.let i,vs,w = s in case w of inl(x) => {<i - 1, x>} | inr(x) => {}
Definitions occuring in Statement :
spreadn: spread3,
lambda: λx.A[x]
,
pair: <a, b>
,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
,
subtract: n - m
,
natural_number: $n
,
single-bag: {x}
,
empty-bag: {}
FDL editor aliases :
collect_filter
collect_filter
collect\_filter() == \mlambda{}s.let i,vs,w = s in case w of inl(x) => \{<i - 1, x>\} | inr(x) => \{\}
Date html generated:
2015_07_17-AM-08_59_12
Last ObjectModification:
2013_03_25-PM-01_54_46
Home
Index