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