Nuprl Definition : loc-Server

loc-Server(f;L0;n0) ==
  RecProcess(<L0, n0>;s,i.if pDVloc?(i)
  then let sndr = pDVloc-id(i) in
           let L,n = s 
           in <<[f L / L], n + 1>, make-lg([<sndr, mk-tagged("msg";pDVloc_tag(f L;nat-to-incomparable(n + 1)))>])>
  else <s, make-lg([])>
  fi )


Definitions occuring in Statement :  pDVloc-id: pDVloc-id(x),  pDVloc?: pDVloc?(x),  pDVloc_tag: pDVloc_tag(id;name),  make-lg: make-lg(L),  rec-process: RecProcess(s0;s,m.next[s; m]),  nat-to-incomparable: nat-to-incomparable(n),  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  let: let,  apply: f a,  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n,  token: "$token",  mk-tagged: mk-tagged(tg;x)
FDL editor aliases :  loc-Server
Latex:
loc-Server(f;L0;n0)  ==
    RecProcess(<L0,  n0>s,i.if  pDVloc?(i)
    then  let  sndr  =  pDVloc-id(i)  in
                      let  L,n  =  s 
                      in  <<[f  L  /  L],  n  +  1>
                            ,  make-lg([<sndr,  mk-tagged("msg";pDVloc\_tag(f  L;nat-to-incomparable(n  +  1)))>])
                            >
    else  <s,  make-lg([])>
    fi  )


Date html generated: 2015_07_23-AM-11_36_25
Last ObjectModification: 2012_08_30-PM-01_47_29

Home Index