Nuprl Definition : es-local-pred

last(P) ==
  fix((λes-local-pred,e. if first(e) then inr (λx.⋅)  if P 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 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-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: 2015_07_20-PM-03_56_39
Last ObjectModification: 2012_07_02-PM-04_11_21

Home Index