Nuprl Definition : class-only-headers
X is a class of type ⌜Interface⌝ such that the only headers in its output
are members of the given list, hdrs.⋅
class-only-headers{i:l}(f;hdrs;X) ==
∀es:EO+(Message(f)). ∀e:E. ∀mi:Interface. (mi ↓∈ X(e) ⇒ (msg-header(mi.msg) ∈ hdrs))
Definitions occuring in Statement :
msg-interface-message: mi.msg,
msg-interface: Interface,
msg-header: msg-header(m),
Message: Message(f),
class-ap: X(e),
event-ordering+: EO+(Info),
es-E: E,
name: Name,
l_member: (x ∈ l),
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs
FDL editor aliases :
class-only-headers
Latex:
class-only-headers\{i:l\}(f;hdrs;X) ==
\mforall{}es:EO+(Message(f)). \mforall{}e:E. \mforall{}mi:Interface. (mi \mdownarrow{}\mmember{} X(e) {}\mRightarrow{} (msg-header(mi.msg) \mmember{} hdrs))
Date html generated:
2016_05_17-PM-03_30_08
Last ObjectModification:
2014_07_17-AM-00_03_58
Theory : messages
Home
Index