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
Latex:
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:
2016_05_16-AM-09_13_28
Last ObjectModification:
2014_02_20-PM-09_45_50
Theory : new!event-ordering
Home
Index