Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactors: Array.feraseIdx: avoid have in definition
otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into `decreasing_by`, the equational theorems are unencumbered by termination arguments. see also leanprover-community/batteries#690 (comment)
- Loading branch information