Nuprl Definition : s-insert

s-insert(x;l) ==
  rec-case(l) of
  [] => [x]
  a::as =>
   v.if (x =z a) then [a / as]
  if x <z 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 ,  lt_int: i <z j,  eq_int: (i =z j)
Definitions occuring in definition :  list_ind: list_ind,  nil: [],  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  cons: [a / b]
FDL editor aliases :  s-insert
Latex:
s-insert(x;l)  ==
    rec-case(l)  of
    []  =>  [x]
    a::as  =>
      v.if  (x  =\msubz{}  a)  then  [a  /  as]
    if  x  <z  a  then  [x;  [a  /  as]]
    else  [a  /  v]
    fi 


Date html generated: 2016_05_14-AM-06_44_49
Last ObjectModification: 2015_12_03-PM-02_07_11

Theory : list_0


Home Index