move meta sections into new files
Open
@chenson2018 is already working on this.
Since Jan 12, 2026.
- Dominant language
- Lean
- Stars
- 709
- Forks
- 200
- Avg merge
- 3d 6h
- Merged PRs (30d)
- 45
Description
In #243 I left some meta sections within other files, specifically in Cslib/Foundations/Data/HasFresh.lean and Cslib/Foundations/Semantics/LTS/Basic.lean. I think it would be less confusing for imports and maybe more performant for these to be in their own files. There is also ReductionSystem, where everything is currently public and exposed.
(I'd like to double check my understand of meta imports first before making any changes.)
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.