Nuprl Definition : es-prior-class-when
(X'?d) when Y == λes,e. if e ∈b Y then {<Y(e), if e ∈b (X)' then (X)'(e) else d fi >} else {} fi
Definitions occuring in Statement :
es-prior-val: (X)',
eclass-val: X(e),
in-eclass: e ∈b X,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
pair: <a, b>,
single-bag: {x},
empty-bag: {}
FDL editor aliases :
es-prior-class-when
Latex:
(X'?d) when Y == \mlambda{}es,e. if e \mmember{}\msubb{} Y then \{<Y(e), if e \mmember{}\msubb{} (X)' then (X)'(e) else d fi >\} else \{\} fi
Date html generated:
2015_07_21-PM-03_48_15
Last ObjectModification:
2012_02_25-PM-02_48_21
Home
Index