Leonardo de Moura 55d5ace68e feat: pattern inference using symbol priorities in grind (#9182) ... This PR tries to improve the E-matching pattern inference for `grind`. That said, we still need better tools for annotating and maintaining `grind` annotations in libraries. closes #9125		2025-07-03 16:47:38 -07:00
..
Basic.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Lemmas.lean	feat: pattern inference using symbol priorities in grind (#9182)	2025-07-03 16:47:38 -07:00