Nuprl Definition : es-interface-state
es-interface-state(X; g) == λes,e. (g X(filter(λe.e ∈b X;≤loc(e))))
Definitions occuring in Statement :
eclass-vals: X(L),
in-eclass: e ∈b X,
es-le-before: ≤loc(e),
filter: filter(P;l),
apply: f a,
lambda: λx.A[x]
Latex:
es-interface-state(X; g) == \mlambda{}es,e. (g X(filter(\mlambda{}e.e \mmember{}\msubb{} X;\mleq{}loc(e))))
Date html generated:
2015_07_20-PM-03_27_01
Last ObjectModification:
2012_02_25-PM-01_46_56
Home
Index