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: f 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: f a
FDL editor aliases :
remove-repeats-fun
Latex:
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