Nuprl Definition : local-pred-class
local-pred-class(P) == λes,e. case last(P es) e of inl(e') => {e'} | inr(x) => {}
Definitions occuring in Statement :
es-local-pred: last(P),
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
single-bag: {x},
empty-bag: {}
FDL editor aliases :
local-pred-class
Latex:
local-pred-class(P) == \mlambda{}es,e. case last(P es) e of inl(e') => \{e'\} | inr(x) => \{\}
Date html generated:
2015_07_20-PM-04_05_26
Last ObjectModification:
2012_02_25-PM-02_01_22
Home
Index