Nuprl Definition : list-max-aux
list-max-aux(x.f[x];L) ==
accumulate (with value a and list item x):
eval n = f[x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
L
with starting value:
inr ⋅ )
Definitions occuring in Statement :
list_accum: list_accum,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
it: ⋅,
pi1: fst(t),
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
list_accum: list_accum,
callbyvalue: callbyvalue,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
pi1: fst(t),
inl: inl x,
pair: <a, b>,
inr: inr x ,
it: ⋅
FDL editor aliases :
list-max-aux
Latex:
list-max-aux(x.f[x];L) ==
accumulate (with value a and list item x):
eval n = f[x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
L
with starting value:
inr \mcdot{} )
Date html generated:
2016_05_14-PM-01_42_37
Last ObjectModification:
2015_09_22-PM-05_54_29
Theory : list_1
Home
Index