Nuprl Definition : fps-alg
fps-alg(X;eq;r) == <PowerSeries(X;r), λf,g. tt, λf,g. tt, λf,g. (f+g), 0, λf.-(f), λf,g. (f*g), 1, λf,g. (inl f), λc,f.\000C (c)*f>
Definitions occuring in Statement :
btrue: tt,
lambda: λx.A[x],
pair: <a, b>,
inl: inl x,
fps-scalar-mul: (c)*f,
fps-mul: (f*g),
fps-neg: -(f),
fps-add: (f+g),
fps-one: 1,
fps-zero: 0,
power-series: PowerSeries(X;r)
FDL editor aliases :
fps-alg
Latex:
fps-alg(X;eq;r) ==
<PowerSeries(X;r), \mlambda{}f,g. tt, \mlambda{}f,g. tt, \mlambda{}f,g. (f+g), 0, \mlambda{}f.-(f), \mlambda{}f,g. (f*g), 1, \mlambda{}f,g. (inl f), \mlambda{}c,\000Cf. (c)*f>
Date html generated:
2016_05_16-AM-08_12_29
Last ObjectModification:
2015_09_23-AM-09_52_27
Theory : instances
Home
Index