leanprover-community / leanprover-community/physlib
Naming in Anomaly Cancellation for QED
Open
@jstoobysmith is already working on this.
Since Apr 20, 2026.
- #1047 by @copilot-swe-agent — closed without merging
help-wanted
- Dominant language
- Lean
- Stars
- 749
- Forks
- 189
- Avg merge
- 1d 21h
- Merged PRs (30d)
- 75
Description
In ./Odd/BasisLinear and ./Even/BasisLinear, there is a poor choice of variable names splitting the two planes.
An example in the odd case is:
compared to:
There should be clearer descriptive naming around these planes. They should also be split into different file systems. The naming is tricky, but I think we should avoid something non-descriptive like plane1 etc.
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.