2cf478cbbe
We recently discovered inconsistencies in Mathlib and Std over the ordering of the arguments for `==`. The most common usage puts the "more variable" term on the LHS, and the "more constant" term on the RHS, however there are plenty of exceptions, and they cause unnecessary pain when switching (particularly, sometimes requiring otherwise unneeded `LawfulBEq` hypotheses). This convention is consistent with the (obvious) preference for `x == 0` over `0 == x` when one term is a literal. We recently updated Std to use this convention https://github.com/leanprover/std4/pull/430 This PR changes the two major places in Lean that use the opposite convention, and adds a suggestion to the docstring for `BEq` about the preferred convention. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||