Nuprl Definition : insert-by

insert-by(eq;r;x;l) ==
  rec-case(l) of
  [] => [x]
  a::as =>
   v.if eq then [a as]
  if then [x; [a as]]
  else [a v]
  fi 



Definitions occuring in Statement :  list_ind: list_ind cons: [a b] nil: [] ifthenelse: if then else fi  apply: a
Definitions occuring in definition :  list_ind: list_ind nil: [] ifthenelse: if then else fi  apply: a cons: [a b]
FDL editor aliases :  insert-by

Latex:
insert-by(eq;r;x;l)  ==
    rec-case(l)  of
    []  =>  [x]
    a::as  =>
      v.if  eq  x  a  then  [a  /  as]
    if  r  x  a  then  [x;  [a  /  as]]
    else  [a  /  v]
    fi 



Date html generated: 2016_05_14-PM-02_34_47
Last ObjectModification: 2015_09_22-PM-05_56_16

Theory : list_1


Home Index