Nuprl Definition : nysiad_on_kdeliver

nysiad_on_kdeliver(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
  λloc,slf,ze,z. let m,s,d = ze in 
                let queue,waiting = z 
                in if loc = d
                   then if isl(s) then <queue @ [<m, s, d>], tt> else <queue, waiting> fi 
                   else <queue, waiting>
                   fi 


Definitions occuring in Statement :  eq_id: a = b,  append: as @ bs,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  isl: isl(x),  btrue: tt,  spreadn: spread3,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  nysiad_on_kdeliver
Latex:
nysiad\_on\_kdeliver(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf)  ==
    \mlambda{}loc,slf,ze,z.  let  m,s,d  =  ze  in 
                                let  queue,waiting  =  z 
                                in  if  loc  =  d
                                      then  if  isl(s)  then  <queue  @  [<m,  s,  d>],  tt>  else  <queue,  waiting>  fi 
                                      else  <queue,  waiting>
                                      fi 


Date html generated: 2015_07_23-PM-03_45_10
Last ObjectModification: 2014_08_06-PM-03_32_11

Home Index