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),
iterate-hdataflow: P*(inputs),
hdf-ap: X(a),
hdataflow: hdataflow(A;B),
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)
FDL editor aliases :
local-class
Latex:
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:
2016_05_16-PM-02_05_06
Last ObjectModification:
2012_08_10-PM-01_15_34
Theory : event-ordering
Home
Index