Skip to content

feat: Add TODOs to QuantumInfo#1091

Merged
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
jstoobysmith:QuantumInfoTODO
May 19, 2026
Merged

feat: Add TODOs to QuantumInfo#1091
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
jstoobysmith:QuantumInfoTODO

Conversation

@jstoobysmith
Copy link
Copy Markdown
Member

Simple PR which

  1. Enables TODO items to be used within QuantumInfo (and hopefully appear on the website).
  2. Adds a single TODO item in the Qubit module as a test.

@jstoobysmith jstoobysmith added the RFC Request for comment label May 13, 2026
@jstoobysmith jstoobysmith requested a review from rodolfor-s May 13, 2026 11:10
rodolfor-s
rodolfor-s previously approved these changes May 19, 2026
Comment thread scripts/MetaPrograms/TODO_to_yml.lean Outdated
Co-authored-by: Rodolfo R. Soldati <rreissol@uwaterloo.ca>
@jstoobysmith jstoobysmith merged commit f2a8463 into leanprover-community:master May 19, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

RFC Request for comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants