Nuprl Definition : list-max-aux

list-max-aux(x.f[x];L) ==
  accumulate (with value and list item x):
   eval f[x] in
   case of inl(p) => if fst(p) <then inl <n, x> else fi  inr(q) => inl <n, x>
  over list:
  with starting value:
   inr ⋅ )

Definitions occuring in Statement :  list_accum: list_accum callbyvalue: callbyvalue ifthenelse: if then else fi  lt_int: i <j it: pi1: fst(t) pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x
Definitions occuring in definition :  list_accum: list_accum callbyvalue: callbyvalue decide: case of inl(x) => s[x] inr(y) => t[y] ifthenelse: if then else fi  lt_int: i <j pi1: fst(t) inl: inl x pair: <a, b> inr: inr  it:
FDL editor aliases :  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:
    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