leanprover-community/batteries

Array.minX functions are buggy

Blei opened this issue · 4 comments

Blei commented

There are two basic bugs: the default value of minD is always used and compared against all entries in the array, instead of only being used as default value if the array is empty:

#eval #[1, 2, 3].minD 0

Expected: 1, actual: 0.

And the case that startPos <= endPos should signify an empty range is not considered:

#eval #[1, 2, 3].min? 1 0

Expected: none, actual: some 2.

kim-em commented

@Blei, I agree, both of these are bugs. Would you be interested in making a PR to fix them?

digama0 commented

The behavior of Array.minD is deliberate, although I agree the naming is bad. (This particular function is useful for expressing what e.g. the value of (arr.push a).min? is.) Any suggestions for alternative names? Maybe Array.min1 or Array.minWith?

Agreed on the second one though.

Blei commented

Yes, I would be interested. As long as you don't care so much about latency in getting this in. :)

So, the plan would be to add new minX functions and rename the ones with the current behaviour to minWithX?

General question: are there plans for unit tests in this standard library?

digama0 commented

General question: are there plans for unit tests in this standard library?

Yes, there are tests in the tests/ directory and you are welcome to add tests for regular functions too, not just tactics. (Then again, for regular functions we usually have theorems in lieu of tests - we want these anyway and they have better coverage than any test suite.) We also (should) have some illustrative tests in the documentation itself.