Nuprl Definition : pi_termco
pi_termco() ==
corec(X.lbl:Atom × if lbl =a "zero" then Unit
if lbl =a "comm" then pre:pi_prefix() × X
if lbl =a "option" then left:X × X
if lbl =a "par" then left:X × X
if lbl =a "rep" then X
if lbl =a "new" then name:Name × X
else Void
fi )
Definitions occuring in Statement :
pi_prefix: pi_prefix(),
name: Name,
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
unit: Unit,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
pi_termco
Latex:
pi\_termco() ==
corec(X.lbl:Atom \mtimes{} if lbl =a "zero" then Unit
if lbl =a "comm" then pre:pi\_prefix() \mtimes{} X
if lbl =a "option" then left:X \mtimes{} X
if lbl =a "par" then left:X \mtimes{} X
if lbl =a "rep" then X
if lbl =a "new" then name:Name \mtimes{} X
else Void
fi )
Date html generated:
2015_07_23-AM-11_31_50
Last ObjectModification:
2014_05_04-PM-08_15_11
Home
Index