Nuprl Definition : mk-extended-eo

mk-extended-eo(type: E;
               domain: dom;
               loc: l;
               info: info;
               causal: R;
               local: locless;
               pred: pred;
               rank: rank) ==
  mk-eo(E;dom;l;R;locless;pred;rank)["info" := info]

Definitions occuring in Statement : mk-eo: mk-eo(E;dom;l;R;locless;pred;rank), token: "$token", record-update: r[x := v]
FDL editor aliases : mk-extended-eo
mk-extended-eo(type: E; domain: dom; loc: l; info: info; causal: R; local: locless; pred: pred; rank: rank) == mk-eo(E;dom;l;R;locless;pred;rank)["info" := info] Date html generated: 2015_07_17-PM-00_01_24 Last ObjectModification: 2014_02_21-AM-00_01_57 Home Index