Nuprl Definition : primed-class-opt
Prior(X)?b == λes,e. case last(λe'.0 <z #(X es e')) e of inl(e') => X es e' | inr(x) => b loc(e)
Definitions occuring in Statement :
es-local-pred: last(P),
es-loc: loc(e),
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)
FDL editor aliases :
primed-class-opt
Latex:
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