Nuprl Definition : remove-combine

remove-combine(cmp;l) ==
  rec-case(l) of
  [] => []
  a::as =>
   v.eval tst = cmp a in
     if (tst =z 0) then as
     if 0 <z tst then [a / as]
     else [a / v]
     fi 


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  apply: f a,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  nil: [],  callbyvalue: callbyvalue,  apply: f a,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  natural_number: $n,  cons: [a / b]
FDL editor aliases :  remove-combine
Latex:
remove-combine(cmp;l)  ==
    rec-case(l)  of
    []  =>  []
    a::as  =>
      v.eval  tst  =  cmp  a  in
          if  (tst  =\msubz{}  0)  then  as
          if  0  <z  tst  then  [a  /  as]
          else  [a  /  v]
          fi 


Date html generated: 2016_05_14-PM-02_41_55
Last ObjectModification: 2015_09_22-PM-05_57_19

Theory : list_1


Home Index