Nuprl Definition : insert-int

insert-int(x;l) ==  rec-case(l) of [] => [x] a::as => v.if (a) < (x)  then eval in [a y]  else [x; [a as]]

Definitions occuring in Statement :  list_ind: list_ind cons: [a b] nil: [] callbyvalue: callbyvalue less: if (a) < (b)  then c  else d
Definitions occuring in definition :  list_ind: list_ind nil: [] less: if (a) < (b)  then c  else d callbyvalue: callbyvalue cons: [a b]
FDL editor aliases :  insert-int

insert-int(x;l)  ==
    rec-case(l)  of
    []  =>  [x]
    a::as  =>
      v.if  (a)  <  (x)    then  eval  y  =  v  in  [a  /  y]    else  [x;  [a  /  as]]

Date html generated: 2017_09_29-PM-05_48_21
Last ObjectModification: 2017_05_03-PM-00_10_41

Theory : list_0

Home Index