Wojciech Różowski d66aaebca6 perf: simplify cbv ite/dite simprocs by reducing Decidable instance directly (#12677) ... This PR changes the approach in `simpIteCbv` and `simpDIteCbv`, by replacing call to `Decidable.decide` with reducing and direct pattern matching on the `Decidable` instance for `isTrue`/`isFalse`. This produces simpler proof terms. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>		2026-03-02 17:11:48 +00:00
..
10067.lean	fix: copied 11940 fix for structure command (#12680)	2026-02-25 13:50:04 +00:00
10850.lean	fix: let Meta.zetaReduce zeta reduce have expressions (#12695)	2026-02-27 00:37:52 +00:00
cbv4.lean	perf: simplify cbv ite/dite simprocs by reducing Decidable instance directly (#12677)	2026-03-02 17:11:48 +00:00
cbv_aes.lean	test: add cbv tests adapted from LNSym (#12694)	2026-02-25 17:08:24 +00:00
cbv_arm_ldst.lean	test: add cbv tests adapted from LNSym (#12694)	2026-02-25 17:08:24 +00:00
mvcgenRflReducibility.lean	fix: heartbeat limit in mvcgen due to withDefault rfl (#12696)	2026-02-26 16:40:42 +00:00
ppFVarsAnonymous.lean	fix: use _fvar._ instead of _ for anonymous fvars (#12745)	2026-03-01 09:59:13 +00:00
test_single.sh