Skip to content

feat: QuantumInfo sorryful results#1092

Merged
jstoobysmith merged 4 commits into
leanprover-community:masterfrom
jstoobysmith:Sorryful
May 24, 2026
Merged

feat: QuantumInfo sorryful results#1092
jstoobysmith merged 4 commits into
leanprover-community:masterfrom
jstoobysmith:Sorryful

Conversation

@jstoobysmith
Copy link
Copy Markdown
Member

Turn on the sorryful result linter for the QuantumInfo directory.

@jstoobysmith
Copy link
Copy Markdown
Member Author

(This will need updating after some of the QuantumInfo PRs have merged)

Comment thread Physlib/Meta/Basic.lean Outdated
@morrison-daniel morrison-daniel added the ready-to-merge This PR is approved and will be merged shortly label May 22, 2026
@morrison-daniel morrison-daniel self-assigned this May 22, 2026
Co-authored-by: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
@jstoobysmith jstoobysmith removed the ready-to-merge This PR is approved and will be merged shortly label May 22, 2026
@jstoobysmith
Copy link
Copy Markdown
Member Author

@morrison-daniel the commit to add your suggestion dismissed your review 😢

@morrison-daniel morrison-daniel added the ready-to-merge This PR is approved and will be merged shortly label May 24, 2026
@jstoobysmith jstoobysmith merged commit 9674ea4 into leanprover-community:master May 24, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants