Nuprl Definition : primed-class
Prior(X) == λes,e. case last(λe'.0 <z #(X es e')) e of inl(e') => X es e' | inr(x) => {}
Definitions occuring in Statement :
es-local-pred: last(P),
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
decide: case b 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