Nuprl Definition : insert-by
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 
Definitions occuring in Statement : 
list_ind: list_ind, 
cons: [a / b]
, 
nil: []
, 
ifthenelse: if b then t else f fi 
, 
apply: f a
Definitions occuring in definition : 
list_ind: list_ind, 
nil: []
, 
ifthenelse: if b then t else f fi 
, 
apply: f 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