Nuprl Definition : local-class
LocalClass(X) ==
∃F:{Id ─→ hdataflow(Info;A)| (∀es:EO+(Info). ∀e:E.
(X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A)))}
Definitions occuring in Statement :
class-ap: X(e),
es-info: info(e),
event-ordering+: EO+(Info),
es-before: before(e),
es-loc: loc(e),
es-E: E,
Id: Id,
map: map(f;as),
pi2: snd(t),
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
equal: s = t ∈ T,
bag: bag(T),
iterate-hdataflow: P*(inputs),
hdf-ap: X(a),
hdataflow: hdataflow(A;B)
FDL editor aliases :
local-class
LocalClass(X) ==
\mexists{}F:\{Id {}\mrightarrow{} hdataflow(Info;A)| (\mforall{}es:EO+(Info). \mforall{}e:E.
(X(e) = (snd(F loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e))))))\}
Date html generated:
2015_07_17-PM-00_31_38
Last ObjectModification:
2012_08_10-PM-01_15_34
Home
Index