Kyle Miller fd926cc44e feat: clean up type annotations when elaborating declaration bodies (#9674) ... This PR cleans up `optParam`/`autoParam`/etc. annotations before elaborating definition bodies, theorem bodies, `fun` bodies, and `let` function bodies. Both `variable`s and binders in declaration headers are supported. There are no changes to `inductive`/`structure`/`axiom`/etc. processing, just `def`/`theorem`/`example`/`instance`.		2025-08-18 04:43:20 +00:00
..
bench	chore: complete riscv_ast benchmark (#9928)	2025-08-15 14:39:25 +00:00
compiler	chore: remove >6 month old deprecations (#9640)	2025-08-05 02:29:15 +00:00
elabissues
ir
lean	feat: clean up type annotations when elaborating declaration bodies (#9674)	2025-08-18 04:43:20 +00:00
pkg	fix: do not allow access to private primitives in public scope (#9890)	2025-08-14 15:34:54 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain