Nuprl Definition : es-local-pred

last(P) ==
  fix((λes-local-pred,e. if first(e) then inr x.⋅)  if pred(e) then inl pred(e) else es-local-pred pred(e) fi ))



Definitions occuring in Statement :  es-first: first(e) es-pred: pred(e) ifthenelse: if then else fi  it: apply: a fix: fix(F) lambda: λx.A[x] inr: inr  inl: inl x
FDL editor aliases :  es-local-pred

Latex:
last(P)  ==
    fix((\mlambda{}es-local-pred,e.  if  first(e)  then  inr  (\mlambda{}x.\mcdot{}) 
                                                if  P  pred(e)  then  inl  pred(e)
                                                else  es-local-pred  pred(e)
                                                fi  ))



Date html generated: 2016_05_16-PM-11_17_51
Last ObjectModification: 2012_07_02-PM-04_11_21

Theory : event-ordering


Home Index