Leonardo de Moura 6e18afac8c feat: kernel hint for proof-by-reflection (#9865) ... This PR adds improved support for proof-by-reflection to the kernel type checker. It addresses the performance issue exposed by #9854. With this PR, whenever the kernel type-checks an argument of the form `eagerReduce _`, it enters "eager-reduction" mode. In this mode, the kernel is more eager to reduce terms. The new `eagerReduce _` hint is often used to wrap `Eq.refl true`. The new hint should not negatively impact any existing Lean package. --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>		2025-08-12 19:24:47 +00:00
..
bench	chore: stabilize benchmark output (#9820)	2025-08-10 10:53:38 +00:00
compiler	chore: remove >6 month old deprecations (#9640)	2025-08-05 02:29:15 +00:00
elabissues
ir
lean	feat: kernel hint for proof-by-reflection (#9865)	2025-08-12 19:24:47 +00:00
pkg	fix: panic on duplicate private def in public section (#9761)	2025-08-06 16:09:18 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain