Nuprl Definition : constrained-msg-interface
Interface(to locs, with hdrs) == {mi:Interface| (mi.dst ∈ locs) ∧ (msg-header(mi.msg) ∈ hdrs)}
Definitions occuring in Statement :
msg-interface-message: mi.msg,
msg-interface-destination: mi.dst,
msg-interface: Interface,
msg-header: msg-header(m),
Id: Id,
name: Name,
l_member: (x ∈ l),
and: P ∧ Q,
set: {x:A| B[x]}
FDL editor aliases :
cmsg
Latex:
Interface(to locs, with hdrs) == \{mi:Interface| (mi.dst \mmember{} locs) \mwedge{} (msg-header(mi.msg) \mmember{} hdrs)\}
Date html generated:
2016_05_17-AM-08_59_40
Last ObjectModification:
2014_07_16-PM-00_16_39
Theory : messages
Home
Index