Nuprl Definition : primed-class-opt

Prior(X)?b ==  λes,e. case last(λe'.0 <#(X es e')) of inl(e') => es e' inr(x) => loc(e)

Definitions occuring in Statement :  es-local-pred: last(P) es-loc: loc(e) lt_int: i <j apply: a lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] natural_number: $n bag-size: #(bs)
FDL editor aliases :  primed-class-opt

Prior(X)?b  ==    \mlambda{}es,e.  case  last(\mlambda{}e'.0  <z  \#(X  es  e'))  e  of  inl(e')  =>  X  es  e'  |  inr(x)  =>  b  loc(e)

Date html generated: 2015_07_21-PM-02_29_54
Last ObjectModification: 2012_02_25-PM-02_02_54

Home Index