Nuprl Definition : delivered-with-headers
delivered-with-headers(hdrs;es;e) ==
mapfilter(
e.<loc(e), info(e)>;e.deq-member(NameDeq;es-header(es;e);hdrs);
loc(e))
Proof not projected
Definitions occuring in Statement :
es-header: es-header(es;e),
es-info: info(e),
es-le-before: loc(e),
es-loc: loc(e),
name-deq: NameDeq,
lambda: x.A[x],
pair: <a, b>,
mapfilter: mapfilter(f;P;L),
deq-member: deq-member(eq;x;L)
FDL editor aliases :
delivered-with-headers
delivered-with-headers(hdrs;es;e) ==
mapfilter(\mlambda{}e.<loc(e), info(e)>\mlambda{}e.deq-member(NameDeq;es-header(es;e);hdrs);\mleq{}loc(e))
Date html generated:
2011_10_20-PM-03_27_33
Last ObjectModification:
2011_09_02-PM-05_16_45
Home
Index