Nuprl Definition : insert-combine

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

Definitions occuring in Statement :  list_ind: list_ind cons: [a b] nil: [] callbyvalue: callbyvalue ifthenelse: if then else fi  lt_int: i <j eq_int: (i =z j) apply: a natural_number: $n
Definitions occuring in definition :  list_ind: list_ind nil: [] callbyvalue: callbyvalue eq_int: (i =z j) apply: a ifthenelse: if then else fi  lt_int: i <j natural_number: $n cons: [a b]
FDL editor aliases :  insert-combine

insert-combine(cmp;f;x;l)  ==
    rec-case(l)  of
    []  =>  [x]
    a::as  =>
      v.eval  tst  =  cmp  x  a  in
          if  (tst  =\msubz{}  0)  then  [f  x  a  /  as]
          if  0  <z  tst  then  [x;  [a  /  as]]
          else  [a  /  v]

Date html generated: 2016_05_14-PM-02_40_37
Last ObjectModification: 2015_09_22-PM-05_57_14

Theory : list_1

Home Index