Nuprl Definition : filter-index

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

Definitions occuring in Statement :  list_ind: list_ind ifthenelse: if then else fi  eq_int: (i =z j) apply: a lambda: λx.A[x] subtract: m add: m natural_number: $n
Definitions occuring in definition :  list_ind: list_ind lambda: λx.A[x] eq_int: (i =z j) add: m subtract: m ifthenelse: if then else fi  apply: a natural_number: $n
FDL editor aliases :  filter-index

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