Traversable.foldr but still refer to rest of data structure?

Stream: new members

[aron]

I want to define a proposition like this:

def EachIsUnique {a} (l : List a) :=
  match l with
  | .nil => True
  | .cons head tail => head ∉ tail ∧ EachIsUnique tail

i.e. that each item is unique across the entire data structure; but I want to make this Prop agnostic as to the underlying data structure.

I feel like this should be doable by generalising over any non-recursive, finite data structure – which I believe in Lean is all of them?

The closest thing I found is the Traversable type class, with its foldr function. But that doesn't quite work. Because I don't just want to fold a single item into an accumulator, but I need to have a way to refer to the data structure as a whole – with the current item sliced off – in each iteration. See how my example does that by recursively matching on the List type and affirming that for each list head, the head is not contained in the tail.

Is there a way to do this using Traversable.foldr? If not, what do you think would be a better way to do this?

[Eric Wieser]

(docs#Traversable.foldr)

[Eric Wieser]

I think you can do this by using foldr to flatten your datatype to a list, then using docs#List.Nodup ?

[Edward van de Meent]

or even skipping foldr and instead using docs#Traversable.toList ?