Nuprl Definition : max_tl_coeffs
max_tl_coeffs(ineqs) == eager-accum(L1,ineq.map2(λx,y. imax(x;|y|);L1;tl(ineq));map(λx.|x|;tl(hd(ineqs)));tl(ineqs))
Definitions occuring in Statement :
eager-accum: eager-accum(x,a.f[x; a];y;l),
map2: map2(f;as;bs),
hd: hd(l),
map: map(f;as),
tl: tl(l),
imax: imax(a;b),
absval: |i|,
lambda: λx.A[x]
Definitions occuring in definition :
map2: map2(f;as;bs),
imax: imax(a;b),
map: map(f;as),
lambda: λx.A[x],
absval: |i|,
hd: hd(l),
tl: tl(l)
FDL editor aliases :
max_tl_coeffs
Latex:
max\_tl\_coeffs(ineqs) ==
eager-accum(L1,ineq.map2(\mlambda{}x,y. imax(x;|y|);L1;tl(ineq));map(\mlambda{}x.|x|;tl(hd(ineqs)));tl(ineqs))
Date html generated:
2016_05_14-AM-07_16_17
Last ObjectModification:
2015_11_26-AM-10_57_06
Theory : omega
Home
Index