Nuprl Definition : last_index

last_index(L;x.P[x]) ==
  snd(accumulate (with value p and list item x):
       let n,lst = p 
       in <n + 1, if P[x] then n + 1 else lst fi >
      over list:
        L
      with starting value:
       <0, 0>))


Definitions occuring in Statement :  list_accum: list_accum,  ifthenelse: if b then t else f fi ,  pi2: snd(t),  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n
Definitions occuring in definition :  pi2: snd(t),  list_accum: list_accum,  spread: spread def,  ifthenelse: if b then t else f fi ,  add: n + m,  pair: <a, b>,  natural_number: $n
FDL editor aliases :  last_index
Latex:
last\_index(L;x.P[x])  ==
    snd(accumulate  (with  value  p  and  list  item  x):
              let  n,lst  =  p 
              in  <n  +  1,  if  P[x]  then  n  +  1  else  lst  fi  >
            over  list:
                L
            with  starting  value:
              ɘ,  0>))


Date html generated: 2016_05_15-PM-04_12_04
Last ObjectModification: 2015_09_23-AM-07_46_48

Theory : general


Home Index