Nuprl Definition : map2
map2(f;as;bs)
==r if as = Ax then [] otherwise if bs = Ax then [] otherwise let a,more_as = as
in let b,more_bs = bs
in eval x = f a b in
eval L = map2(f;more_as;more_bs) in
[x / L]
map2(f;as;bs) ==
fix((λmap2,as,bs. if as = Ax then [] otherwise if bs = Ax then [] otherwise let a,more_as = as
in let b,more_bs = bs
in eval x = f a b in
eval L = map2 more_as more_bs in
[x / L]))
as
bs
Definitions occuring in Statement :
cons: [a / b],
nil: [],
callbyvalue: callbyvalue,
isaxiom: if z = Ax then a otherwise b,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
isaxiom: if z = Ax then a otherwise b,
nil: [],
spread: spread def,
callbyvalue: callbyvalue,
apply: f a,
cons: [a / b]
FDL editor aliases :
map2
Latex:
map2(f;as;bs)
==r if as = Ax then []
otherwise if bs = Ax then [] otherwise let a,more$_{as}$ = as
in let b,more$_{bs}$ = bs
in eval x = f a b in
eval L = map2(f;more$_{as}$;mor\000Ce$_{bs}$) in
[x / L]
Latex:
map2(f;as;bs) ==
fix((\mlambda{}map2,as,bs. if as = Ax then []
otherwise if bs = Ax then [] otherwise let a,more$_{as}$ = a\000Cs
in let b,more$_{bs}$ \000C= bs
in eval x = f a b in
eval L = map2 more$_{as\000C}$ more$_{bs}$ in
[x / L]))
as
bs
Date html generated:
2016_05_14-AM-06_42_53
Last ObjectModification:
2015_12_03-PM-02_06_40
Theory : list_0
Home
Index