Nuprl Definition : remove-repeats-fun

remove-repeats-fun(eq;f;L) ==  rec-case(L) of [] => [] a::as => r.[a filter(λx.(¬b(eq (f x) (f a)));r)]

Definitions occuring in Statement :  filter: filter(P;l) list_ind: list_ind cons: [a b] nil: [] bnot: ¬bb apply: a lambda: λx.A[x]
Definitions occuring in definition :  list_ind: list_ind nil: [] cons: [a b] filter: filter(P;l) lambda: λx.A[x] bnot: ¬bb apply: a
FDL editor aliases :  remove-repeats-fun

remove-repeats-fun(eq;f;L)  ==
    rec-case(L)  of
    []  =>  []
    a::as  =>
      r.[a  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  (f  x)  (f  a)));r)]

Date html generated: 2016_05_14-PM-03_28_18
Last ObjectModification: 2015_09_22-PM-05_59_47

Theory : decidable!equality

Home Index