Data.Fintype.Array

Stream: mathlib4

[Yury G. Kudryashov]

Since length of an Array is no longer fixed, should we port Data.Fintype.Array?

[Ruben Van de Velde]

Earlier thread at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/porting.20.60.2Earray.60.20files.20whose.20PR's.20were.20closed.3F

[Thomas Murrills]

We could maybe translate the existing fintype defs for List, which I believe are about duplicate-free lists, since that’s what you might expect to find in a file of that name. (Re: earlier discussion, hopefully such manual translations won’t always be necessary, but they seem to be for now.)

We don’t necessarily need to do this during the port though, and I think there’s an argument for just commenting the whole file out and leaving a porting note.

[Yury G. Kudryashov]

The existing instances are about arrays of fixed length.

[Yury G. Kudryashov]

file3#data/fintype/array

[Thomas Murrills]

I’m talking about the existing instances for List. Those could be translated to mathlib4’s Array and might belong in this file.

[Thomas Murrills]

These aren’t actually for List per se, but for lists without duplicate elements.

[Yury G. Kudryashov]

IMHO, this is not a part of the porting.

[Yury G. Kudryashov]

And it should be done by someone who understands how to make an implementation that doesn't rebuild arrays from lists lots of times.

[Thomas Murrills]

I agree, that’s why I said there’s an argument for not doing this during the port. :) I’m just saying the file itself could contain something meaningful and therefore could have a future in mathlib4 (and so could be “ported” with no real code in it and a TODO note)

[Eric Wieser]

I've ported this at #5792 to get it off the dashboard. The file only contains two results; one is un-stateable in current mathlib4, while the other is just false for the new Array, and we already have the true version for Vector.