4 commits

Author	SHA1	Message	Date
Kim Morrison	eccc472e8d	chore: remove set_option grind.warning false (#8714) ... This PR removes the now unnecessary `set_option grind.warning false` statements, now that the warning is disabled by default.	2025-06-11 05:09:19 +00:00
Leonardo de Moura	2c8ee4f29c	fix: simplify interface between grind core and cutsat (#8564) ... This PR simplifies the interface between the `grind` core and the cutsat procedure. Before this PR, core would try to minimize the number of numeric literals that have to be internalized in cutsat. This optimization was buggy (see `grind_cutsat_zero.lean` test), and produced counterintuitive counterexamples.	2025-05-31 16:28:31 +00:00
Leonardo de Moura	068e0b7215	chore: %reset_grind_attrs ==> reset_grind_attrs% (#7722) ... Ensure the grind reset command follows our command naming conventions.	2025-03-29 17:18:07 +00:00
Leonardo de Moura	9466c5db25	fix: constant patterns in grind (#7689) ... This PR fixes the support for "constant patterns" in `grind`. Example: ```lean def a := 10 example : a = 5 + 5 := by grind [a] ```	2025-03-26 19:07:21 +00:00