Wojciech Różowski f3b8f76ec4 test: add cbv benchmark for evaluating Decidable.decide (#12467) ... This PR adds a benchmark for `cbv` tactic for evaluating `Decidable.decide` for a `Decidable` instance for a problem of checking if a number is not a prime power. The test has been inspired by a recent discussion on the [leanprover zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can't.20decide.20if.2015.20is.20a.20prime.20power/with/572513330).		2026-02-13 13:25:35 +00:00
..
decide.lean	test: add cbv benchmark for evaluating Decidable.decide (#12467)	2026-02-13 13:25:35 +00:00
dedup.lean
divisors.lean
leroy.lean	refactor: main loop of the cbv tactic (#12417)	2026-02-11 11:47:18 +00:00