Nuprl Definition : pi_prefix
pi_prefix() == lbl:Atom × if lbl =a "send" then chan:Name × Name if lbl =a "rcv" then chan:Name × Name else Void fi
Definitions occuring in Statement :
name: Name,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
pi_prefix
Latex:
pi\_prefix() ==
lbl:Atom \mtimes{} if lbl =a "send" then chan:Name \mtimes{} Name
if lbl =a "rcv" then chan:Name \mtimes{} Name
else Void
fi
Date html generated:
2015_07_23-AM-11_31_17
Last ObjectModification:
2014_05_04-PM-07_44_38
Home
Index