Nuprl Definition : select-tagged-indices-aux

select-tagged-indices-aux(P;tg;L) ==
  rec-case(L) of
  [] => λn.[]
  fst::rest =>
   r.if P fst then λn.[<n, tg fst> / (r (n + 1))] else λn.(r (n + 1)) fi 


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  add: n + m,  natural_number: $n
FDL editor aliases :  select-tagged-indices-aux
Latex:
select-tagged-indices-aux(P;tg;L)  ==
    rec-case(L)  of
    []  =>  \mlambda{}n.[]
    fst::rest  =>
      r.if  P  fst  then  \mlambda{}n.[<n,  tg  fst>  /  (r  (n  +  1))]  else  \mlambda{}n.(r  (n  +  1))  fi 


Date html generated: 2015_07_23-AM-11_36_35
Last ObjectModification: 2012_08_30-PM-01_47_46

Home Index