Nuprl Definition : filter-index

filter-index(P;L) ==
  rec-case(L) of
  [] => λi.i
  u::v =>
   r.λi.if (i =z 0) then 0 else (r (i - 1)) + if P u then 1 else 0 fi  fi 


Definitions occuring in Statement :  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  lambda: λx.A[x],  eq_int: (i =z j),  add: n + m,  subtract: n - m,  ifthenelse: if b then t else f fi ,  apply: f a,  natural_number: $n
FDL editor aliases :  filter-index
Latex:
filter-index(P;L)  ==
    rec-case(L)  of
    []  =>  \mlambda{}i.i
    u::v  =>
      r.\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  (r  (i  -  1))  +  if  P  u  then  1  else  0  fi    fi 


Date html generated: 2016_05_14-AM-07_50_42
Last ObjectModification: 2015_09_22-PM-05_54_04

Theory : list_1


Home Index