Nuprl Definition : es-interface-prior-vals
X(≤e) ==
fix((λes-interface-prior-vals,e. (if e ∈b X then [X(e)] else [] fi
@ if first(e) then [] else es-interface-prior-vals pred(e) fi )))
e
Definitions occuring in Statement :
eclass-val: X(e),
in-eclass: e ∈b X,
es-first: first(e),
es-pred: pred(e),
append: as @ bs,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x]
FDL editor aliases :
es-interface-prior-vals
Latex:
X(\mleq{}e) ==
fix((\mlambda{}es-interface-prior-vals,e. (if e \mmember{}\msubb{} X then [X(e)] else [] fi
@ if first(e) then [] else es-interface-prior-vals pred(e) fi )))
e
Date html generated:
2015_07_20-PM-03_43_50
Last ObjectModification:
2012_07_02-PM-04_11_09
Home
Index