Nuprl Definition : eclass-cond
eclass-cond(X;Y) == λes,e. if e ∈b X then eclass3(X;Y)(e) else Y(e) fi
Definitions occuring in Statement :
eclass3: eclass3(X;Y),
member-eclass: e ∈b X,
class-ap: X(e),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x]
FDL editor aliases :
eclass-cond
eclass-cond(X;Y) == \mlambda{}es,e. if e \mmember{}\msubb{} X then eclass3(X;Y)(e) else Y(e) fi
Date html generated:
2015_07_17-PM-00_38_06
Last ObjectModification:
2012_08_15-PM-04_34_53
Home
Index