Sebastian Ullrich 6ab20e7f03 chore: revert "feat: default let rec and where decls to private under the module system" (#9743) ... Stage 2 tests broke, to be fixed tomorrow Reverts leanprover/lean4#9666		2025-08-05 21:28:08 +00:00
..
Module	chore: revert "feat: default let rec and where decls to private under the module system" (#9743)	2025-08-05 21:28:08 +00:00
lakefile.toml
lean-toolchain
Module.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
test.sh