Nuprl Definition : mk-vs
Point= V zero= z x+y= +[x; y] a*u= *[a; u] == λx.x["Point" := V]["0" := z]["+" := λx,y. +[x; y]]["*" := λa,u. *[a; u]]
Definitions occuring in Statement :
lambda: λx.A[x],
token: "$token",
record-update: r[x := v]
Definitions occuring in definition :
record-update: r[x := v],
token: "$token",
lambda: λx.A[x]
FDL editor aliases :
mk-vs
Latex:
Point= V
zero= z
x+y= +[x; y]
a*u= *[a; u] ==
\mlambda{}x.x["Point" := V]["0" := z]["+" := \mlambda{}x,y. +[x; y]]["*" := \mlambda{}a,u. *[a; u]]
Date html generated:
2018_05_22-PM-09_41_44
Last ObjectModification:
2017_11_02-PM-04_38_48
Theory : linear!algebra
Home
Index