Nuprl Definition : es-local-prior-state

prior-state(f;base;X;e) ==
  fix((λes-local-prior-state,e. if e ∈b prior(X) then f (es-local-prior-state prior(X)(e)) X(prior(X)(e)) else base fi )\000C) e


Definitions occuring in Statement :  es-prior-interface: prior(X),  eclass-val: X(e),  in-eclass: e ∈b X,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x]
FDL editor aliases :  es-local-prior-state
Latex:
prior-state(f;base;X;e)  ==
    fix((\mlambda{}es-local-prior-state,e.  if  e  \mmember{}\msubb{}  prior(X)
                                                              then  f  (es-local-prior-state  prior(X)(e))  X(prior(X)(e))
                                                              else  base
                                                              fi  )) 
    e


Date html generated: 2015_07_21-PM-03_42_00
Last ObjectModification: 2012_07_02-PM-04_13_35

Home Index