Skip to content

refactor: Optional linters for Quantum Info#1212

Open
jstoobysmith wants to merge 2 commits into
leanprover-community:masterfrom
jstoobysmith:quantumInfoLinters
Open

refactor: Optional linters for Quantum Info#1212
jstoobysmith wants to merge 2 commits into
leanprover-community:masterfrom
jstoobysmith:quantumInfoLinters

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Include QuantumInfo the QuantumInfo library within the linters, but include them all in an exemptions file. This means that we can go through file by file and get them passing the linters.

The code here was generated using Claude Opus 4.8. But I have checked it is all sound and have checked it all works as it should.

@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant