Nuprl Definition : insert-no-combine

insert-no-combine(cmp;x;l) ==  rec-case(l) of [] => [x] a::as => v.if 0 ≤cmp then [x; [a as]] else [a v] fi 

Definitions occuring in Statement :  list_ind: list_ind cons: [a b] nil: [] le_int: i ≤j ifthenelse: if then else fi  apply: a natural_number: $n
Definitions occuring in definition :  list_ind: list_ind nil: [] ifthenelse: if then else fi  le_int: i ≤j natural_number: $n apply: a cons: [a b]
FDL editor aliases :  insert-no-combine

insert-no-combine(cmp;x;l)  ==
    rec-case(l)  of
    []  =>  [x]
    a::as  =>
      v.if  0  \mleq{}z  cmp  x  a  then  [x;  [a  /  as]]  else  [a  /  v]  fi 

Date html generated: 2016_05_14-PM-02_42_52
Last ObjectModification: 2015_09_22-PM-05_57_26

Theory : list_1

Home Index