Nuprl Definition : nysiad_headers_fun
nysiad_headers_fun(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
λhdr.if name_eq(hdr;readyhdr) then Id
if name_eq(hdr;add2baghdr) then Message(mf) × Id? × Id
if name_eq(hdr;addwaitinghdr) then Message(mf) × Id? × Id
if name_eq(hdr;adeliverhdr) then Id × Message(mf)
if name_eq(hdr;inputmsghdr) then Message(mf) × Id? × Id
if name_eq(hdr;tooarcasthdr) then Message(mf) × Id? × Id
if name_eq(hdr;kdeliverhdr) then Message(mf) × Id? × Id
else Top
fi
Definitions occuring in Statement :
Message: Message(f),
Id: Id,
name_eq: name_eq(x;y),
ifthenelse: if b then t else f fi ,
top: Top,
unit: Unit,
lambda: λx.A[x],
product: x:A × B[x],
union: left + right
FDL editor aliases :
nysiad_headers_fun
Latex:
nysiad\_headers\_fun(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf) ==
\mlambda{}hdr.if name\_eq(hdr;readyhdr) then Id
if name\_eq(hdr;add2baghdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;addwaitinghdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;adeliverhdr) then Id \mtimes{} Message(mf)
if name\_eq(hdr;inputmsghdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;tooarcasthdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;kdeliverhdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
else Top
fi
Date html generated:
2015_07_23-PM-03_40_46
Last ObjectModification:
2014_08_06-PM-03_23_09
Home
Index