Nuprl Definition : mk-eo-record
mk-eo-record(E;dom;l;R;locless;pred;rank) ==
λx.x["E" := E]["dom" := dom]["loc" := l]["<" := R]["locless" := locless]["pred" := pred]["rank" := rank]
Definitions occuring in Statement :
lambda: λx.A[x],
token: "$token",
record-update: r[x := v]
FDL editor aliases :
mk-eo-record
mk-eo-record(E;dom;l;R;locless;pred;rank) ==
\mlambda{}x.x["E" := E]["dom" := dom]["loc" := l]["<" := R]["locless" := locless]["pred" := pred]
["rank" := rank]
Date html generated:
2015_07_17-AM-08_33_49
Last ObjectModification:
2014_02_20-PM-09_45_50
Home
Index