Nuprl Definition : primed-class

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



Definitions occuring in Statement :  es-local-pred: last(P) 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) empty-bag: {}
FDL editor aliases :  primed-class

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



Date html generated: 2015_07_21-PM-02_29_35
Last ObjectModification: 2012_02_25-PM-02_02_42

Home Index