Nuprl Definition : rat_termco
rat_termco() ==
corec(X.lbl:Atom × if lbl =a "Constant" then ℤ
if lbl =a "Var" then ℤ
if lbl =a "Add" then left:X × X
if lbl =a "Subtract" then left:X × X
if lbl =a "Multiply" then left:X × X
if lbl =a "Divide" then num:X × X
if lbl =a "Minus" then X
else Void
fi )
Definitions occuring in Statement :
corec: corec(T.F[T])
,
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
product: x:A × B[x]
,
int: ℤ
,
token: "$token"
,
atom: Atom
,
void: Void
Definitions occuring in definition :
corec: corec(T.F[T])
,
atom: Atom
,
int: ℤ
,
product: x:A × B[x]
,
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
token: "$token"
,
void: Void
FDL editor aliases :
rat_termco
Latex:
rat\_termco() ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Constant" then \mBbbZ{}
if lbl =a "Var" then \mBbbZ{}
if lbl =a "Add" then left:X \mtimes{} X
if lbl =a "Subtract" then left:X \mtimes{} X
if lbl =a "Multiply" then left:X \mtimes{} X
if lbl =a "Divide" then num:X \mtimes{} X
if lbl =a "Minus" then X
else Void
fi )
Date html generated:
2019_10_16-PM-03_07_52
Last ObjectModification:
2019_03_31-PM-05_15_28
Theory : reals
Home
Index