Nuprl Definition : es-interface-pred
X-pred == λe.if e ∈b prior(X) then prior(X)(e) else e fi
Definitions occuring in Statement :
es-prior-interface: prior(X),
eclass-val: X(e),
in-eclass: e ∈b X,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x]
FDL editor aliases :
es-interface-pred
Latex:
X-pred == \mlambda{}e.if e \mmember{}\msubb{} prior(X) then prior(X)(e) else e fi
Date html generated:
2015_07_21-PM-03_30_34
Last ObjectModification:
2012_02_25-PM-02_29_02
Home
Index