Leonardo de Moura 8735447d44 feat: infrastructure for NatModule in grind linarith (#10267) ... This PR implements the infrastructure for supporting `NatModule` in `grind linarith` and uses it to handle disequalities. Another PR will add support for equalities and inequalities. Example: ```lean open Lean Grind variable (M : Type) [NatModule M] [AddRightCancel M] example (x y : M) : 2 • x + 3 • y + x = 3 • (x + y) := by grind ```		2025-09-06 01:16:03 +00:00
..
bench	perf: improve iterator/range benchmarks, use shortcut instances for Int ranges (#10197)	2025-09-03 15:47:52 +00:00
compiler	fix: Unicode path support for Lean Windows executables (#10133)	2025-08-27 11:28:55 +00:00
elabissues
ir
lean	feat: infrastructure for NatModule in grind linarith (#10267)	2025-09-06 01:16:03 +00:00
pkg	perf: rebuild leak on private match (#10246)	2025-09-04 12:51:42 +00:00
playground	feat: linear-size DecidableEq instance (#10152)	2025-09-03 06:31:49 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain