Nuprl Definition : runEvents
runEvents(r) == {tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}
Definitions occuring in Statement :
is-run-event: is-run-event(r;t;x),
Id: Id,
nat: ℕ,
assert: ↑b,
pi1: fst(t),
pi2: snd(t),
set: {x:A| B[x]} ,
product: x:A × B[x]
FDL editor aliases :
runEvents
Latex:
runEvents(r) == \{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(r;fst(tx);snd(tx))\}
Date html generated:
2015_07_23-AM-11_10_31
Last ObjectModification:
2012_02_25-PM-03_40_52
Home
Index