UnionFind on nightly-testing

Stream: batteries

[Kim Morrison]

Just cross-posting here that I wouldn't mind assistance repairing UnionFind on nightly-testing, where it is currently broken because of the change to Array.get arguments.

So far besides UnionFind this change has been very pleasant. I suspect it is fine in UnionFind too, I just wanted to move on the Mathlib with my available time.

[Kim Morrison]

(And pre-empting the "but I like Array.get as it was", we can add Array.fget if it is needed.)

[Mario Carneiro]

I don't understand why this change is happening, but one thing I can say is that the GetElem instance for Fin is now majorly problematic with the new simp normal forms

[Shreyas Srinivas]

This is bound to break a lot of array code that uses Array.get

[François G. Dorais]

IMHO, it should have always been get (i : Nat) (h : ...), uget (i : USize) (h : ...), fget (i : Fin ...). I view this as a step in the right direction from a "revisionist" perspective.

[Kim Morrison]

Note that right at this moment we don't actually have Array.fget anywhere. I'm not quite certain where/when that will land, as it presently doesn't seem urgent, but I'm sure it will at some point.