Sebastian Ullrich b42a7780e2 feat: default let rec and where decls to private under the module system (#9666) ... This PR addresses an outstanding feature in the module system to automatically mark `let rec` and `where` helper declarations as private unless they are defined in a public context such as under `@[expose]`.		2025-08-05 11:41:28 +00:00
..
Module	feat: default let rec and where decls to private under the module system (#9666)	2025-08-05 11:41:28 +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