Leonardo de Moura a4496a4a6b chore: remove grind +ringNull option (#9954) ... This PR removes the option `grind +ringNull`. It provided an alternative proof term construction for the `grind ring` module, but it was less effective than the default proof construction mode and had effectively become dead code. This PR also optimizes semiring normalization proof terms using the infrastructure added in #9946. **Remark:** After updating stage0, we can remove several background theorems from the `Init/Grind` folder.		2025-08-17 23:04:59 +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	chore: remove grind +ringNull option (#9954)	2025-08-17 23:04:59 +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