Nuprl Definition : es-last-event
es-last-event(es;P;e) ==
fix((λes-last-event,e. if P e then inl e if first(e) then inr (λx.⋅) else es-last-event pred(e) fi )) e
Definitions occuring in Statement :
es-first: first(e),
es-pred: pred(e),
ifthenelse: if b then t else f fi ,
it: ⋅,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
inr: inr x ,
inl: inl x
FDL editor aliases :
es-last-event
es-last-event
es-last-event(es;P;e) ==
fix((\mlambda{}es-last-event,e. if P e then inl e
if first(e) then inr (\mlambda{}x.\mcdot{})
else es-last-event pred(e)
fi ))
e
Date html generated:
2015_07_17-AM-08_39_24
Last ObjectModification:
2013_03_25-PM-01_37_03
Home
Index