Arthur Adjedj bf8b66c6a5 fix: ignore unused alternatives in Ord derive handler (#3725) ... Closes #3706 This derive handler's implementation is very similar to `BEq`'s, which already ignores unused alternative so as to work correctly on indexed inductive types. This PR simply implements the same solution as the one present in [`BEq.lean`](2c15cdda04/src/Lean/Elab/Deriving/BEq.lean (L94)). After some tests, it doesn't seem like any other derive handler present in Core suffers from the same issue (though some handlers don't work on indexed inductives for other reasons).		2024-03-21 10:29:22 +00:00
..
bench	test: add language server startup benchmark (#3558)	2024-03-04 09:01:51 +00:00
compiler	fix: do not dllexport symbols in core static libraries (#3601)	2024-03-15 11:58:34 +00:00
elabissues
ir
lean	fix: ignore unused alternatives in Ord derive handler (#3725)	2024-03-21 10:29:22 +00:00
pkg	feat: allow duplicate theorems to be imported	2024-03-13 12:57:41 -07:00
playground	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508)	2024-03-04 23:56:30 +00:00
plugin	fix: do not dllexport symbols in core static libraries (#3601)	2024-03-15 11:58:34 +00:00
simpperf
.gitignore
common.sh
lean-toolchain