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
Latex:
collect\_filter() == \mlambda{}s.let i,vs,w = s in case w of inl(x) => \{<i - 1, x>\} | inr(x) => \{\}
Date html generated:
2016_05_16-AM-10_09_28
Last ObjectModification:
2013_03_25-PM-01_54_46
Theory : new!event-ordering
Home
Index