Nuprl Definition : pax-msgs-well-typed

pax-msgs-well-typed(Result;es) ==

e:E
    let msg = info(e) in
     let hdr = msg-header(msg) in
     let typ = msg-type(msg) in
     (

isl(pax-header2type(Result;hdr)))

(typ

r outl(pax-header2type(Result;hdr)))

Proof not projected

Definitions occuring in Statement : pax-header2type: pax-header2type(Result;hdr), msg-header: msg-header(m), msg-type: msg-type(msg), es-info: info(e), es-E: E, subtype_rel: A

r B, outl: outl(x), isl: isl(x), assert:

b, let: let, all:

x:A. B[x], implies: P

Q
Definitions : all:

x:A. B[x], es-E: E, es-info: info(e), msg-header: msg-header(m), let: let, msg-type: msg-type(msg), implies: P

Q, assert:

b, isl: isl(x), subtype_rel: A

r B, outl: outl(x), pax-header2type: pax-header2type(Result;hdr)
FDL editor aliases : pax-msgs-well-typed

pax-msgs-well-typed(Result;es) == \mforall{}e:E let msg = info(e) in let hdr = msg-header(msg) in let typ = msg-type(msg) in (\muparrow{}isl(pax-header2type(Result;hdr))) {}\mRightarrow{} (typ \msubseteq{}r outl(pax-header2type(Result;hdr))) Date html generated: 2011_10_20-PM-11_50_08 Last ObjectModification: 2011_05_12-PM-05_46_56 Home Index