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