Nuprl Definition : delivered-with-headers
delivered-with-headers(hdrs;es;e) == mapfilter(λe.<loc(e), info(e)>;λe.header(e) ∈b hdrs);≤loc(e))
Definitions occuring in Statement :
es-header: header(e),
es-info: info(e),
es-le-before: ≤loc(e),
es-loc: loc(e),
name-deq: NameDeq,
deq-member: x ∈b L),
mapfilter: mapfilter(f;P;L),
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
delivered-with-headers
Latex:
delivered-with-headers(hdrs;es;e) == mapfilter(\mlambda{}e.<loc(e), info(e)>\mlambda{}e.header(e) \mmember{}\msubb{} hdrs);\mleq{}loc(e))
Date html generated:
2015_07_21-PM-04_51_18
Last ObjectModification:
2012_11_29-PM-06_20_25
Home
Index