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: 2015_07_22-AM-11_58_54
Last ObjectModification: 2014_07_16-PM-00_16_39

Home Index