Nuprl Definition : run-event-interval
run-event-interval(r;e1;e2) ==
let x = run-event-loc(e1) in
mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[run-event-step(e1), run-event-step(e2) + 1))
Definitions occuring in Statement :
run-event-step: run-event-step(e),
run-event-loc: run-event-loc(e),
is-run-event: is-run-event(r;t;x),
from-upto: [n, m),
mapfilter: mapfilter(f;P;L),
let: let,
lambda: λx.A[x],
pair: <a, b>,
add: n + m,
natural_number: $n
FDL editor aliases :
run-event-interval
Latex:
run-event-interval(r;e1;e2) ==
let x = run-event-loc(e1) in
mapfilter(\mlambda{}t.<t, x>\mlambda{}t.is-run-event(r;t;x);[run-event-step(e1), run-event-step(e2) + 1))
Date html generated:
2015_07_23-AM-11_11_25
Last ObjectModification:
2012_02_25-PM-03_41_44
Home
Index