Batteries#925

Stream: batteries

[Shreyas Srinivas]

In the context of PR batteries#925 I was going through the definitions in Init.Data.Array.Basic in core. There are two successive definitions modify and modifyOp. I am not sure why they are different since modifyOp just calls modify.

[Shreyas Srinivas]

I am inclined to drop modifyOp for Vectors. Is this fine?

[Shreyas Srinivas]

Some help needed: In the process of proving that modify does not change a Vector's size, I came across Array.size_modifyM which is using this strange Satisfies predicate. I am not quite sure how to put this lemma to use.

[Shreyas Srinivas]

Reference: https://github.com/leanprover-community/batteries/pull/925/files#r1720862336

[Shreyas Srinivas]

There are two other sorries (3 in total)

2. https://github.com/leanprover-community/batteries/pull/925/files#r1720862908
3. https://github.com/leanprover-community/batteries/pull/925/files#r1720862960

[Mario Carneiro]

I think modifyOp is vestigial, it was originally intended for the a[i] := e syntax but I'm not sure it was ever implemented

[Mario Carneiro]

it is similar to getOp which was the a[i] syntax, now powered by the GetElem typeclass

[Shreyas Srinivas]

Apart from the sorrys only docstrings remain.

[Shreyas Srinivas]

I still have to hunt for monadic defs elsewhere. EDIT : Found all the defs suitable for this PR as far as I can see.