Nuprl Definition : alist-map
alist-map(eq;L) == λx.case apply-alist(eq;L;x) of inl(x') => x' | inr(_) => x
Definitions occuring in Statement :
apply-alist: apply-alist(eq;L;x),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply-alist: apply-alist(eq;L;x)
FDL editor aliases :
alist-map
Latex:
alist-map(eq;L) == \mlambda{}x.case apply-alist(eq;L;x) of inl(x') => x' | inr($_{}$) =>\000C x
Date html generated:
2020_05_19-PM-09_50_51
Last ObjectModification:
2020_01_26-PM-10_26_27
Theory : list_1
Home
Index