Listable types

Stream: mathlib4

[Adam Topaz]

What's the canonical way to speak about finite types X where there is a list L : List X with no duplicates where L.toFinset = Finset.elems?

One way is to say something like this:

example {X : Type*} [Fintype X] [LinearOrder X] : List X :=
  Finset.univ.sort (· ≤ ·)

And this is indeed equivalent since a list L as above induces a linear order in the obvious way. But is this the right way to do this?

[Yaël Dillies]

@Anne Baanen and I had a PR in Lean 3 to add a typeclass for such types, but it never landed.

[Adam Topaz]

What class did you use? Or did you make a new class?

[Yaël Dillies]

We were making a new one.

[Yaël Dillies]

Nowadays you have docs#FinEnum (although I'm not sure what the motivation for it was) for Fin-indexed tuples, and I have a version of it which further contains a List (for defeq convenience) in my second-year computing project.

[Adam Topaz]

Ok, I guess FinEnum accomplishes the same thing.

[Yaël Dillies]

I guess it depends what you want to do with it. Do you want to run code?

[Adam Topaz]

yeah

[Adam Topaz]

it looks computable enough!?

[Yaël Dillies]

Then probably you need my version, which instead contains a List (or an Array)

[Adam Topaz]

There's docs#FinEnum.toList

[Adam Topaz]

that should be good enough for me.

[Yaël Dillies]

Okay! Ring me up if not.

[Eric Wieser]

It's computable only in the weakest sense, the implementation is pretty computationally awful and goes back and forth between lists everywhere