Nuprl Definition : type-of-message

type-of-message(es;nm;locs;T) ==

e:E(Base([nm])@locs). (msg-type(Base([nm])@locs(e))

r T)

Proof not projected

Definitions occuring in Statement : base-locs-headers: Base(hdrs)@locs, msg-type: msg-type(msg), es-E-interface: E(X), eclass-val: X(e), subtype_rel: A

r B, all:

x:A. B[x], cons: [car / cdr], nil: []
Definitions : all:

x:A. B[x], es-E-interface: E(X), subtype_rel: A

r B, msg-type: msg-type(msg), eclass-val: X(e), base-locs-headers: Base(hdrs)@locs, cons: [car / cdr], nil: []
FDL editor aliases : type-of-message

type-of-message(es;nm;locs;T) == \mforall{}e:E(Base([nm])@locs). (msg-type(Base([nm])@locs(e)) \msubseteq{}r T) Date html generated: 2011_10_20-PM-04_53_11 Last ObjectModification: 2011_05_24-AM-11_20_30 Home Index