Nuprl Definition : pi_prefix_ind

pi_prefix_ind(v;
              pisend(chan,var)⇒ send[chan; var];
              pircv(chan,var)⇒ rcv[chan; var])  ==
  let lbl,v1 = v 
  in if lbl="send" then let chan,v2 = v1 in send[chan; v2]
     if lbl="rcv" then let chan,v2 = v1 in rcv[chan; v2]
     else ⊥
     fi 


Definitions occuring in Statement :  bottom: ⊥,  atom_eq: if a=b then c else d fi ,  spread: spread def,  token: "$token"
FDL editor aliases :  pi_prefix_ind pi_prefix_ind
Latex:
pi\_prefix\_ind(v;
                            pisend(chan,var){}\mRightarrow{}  send[chan;  var];
                            pircv(chan,var){}\mRightarrow{}  rcv[chan;  var])    ==
    let  lbl,v1  =  v 
    in  if  lbl="send"  then  let  chan,v2  =  v1  in  send[chan;  v2]
          if  lbl="rcv"  then  let  chan,v2  =  v1  in  rcv[chan;  v2]
          else  \mbot{}
          fi 


Date html generated: 2015_07_23-AM-11_31_46
Last ObjectModification: 2014_05_04-PM-07_45_34

Home Index