Nuprl Definition : eo-restrict
eo-restrict(eo;P) == eo["dom" := λe.((eo."dom" e) ∧b (P e))]
Definitions occuring in Statement :
band: p ∧b q,
apply: f a,
lambda: λx.A[x],
token: "$token",
record-update: r[x := v],
record-select: r.x
FDL editor aliases :
eo-restrict
eo-restrict
eo-restrict(eo;P) == eo["dom" := \mlambda{}e.((eo."dom" e) \mwedge{}\msubb{} (P e))]
Date html generated:
2015_07_17-AM-08_34_04
Last ObjectModification:
2013_03_22-PM-08_58_14
Home
Index