Skip to content

docs(ClassicalMechanics): expand the module overview - #1482

Merged
jstoobysmith merged 1 commit into
leanprover-community:masterfrom
sankalpsthakur:agent/classical-mechanics-module-docs
Aug 2, 2026
Merged

docs(ClassicalMechanics): expand the module overview#1482
jstoobysmith merged 1 commit into
leanprover-community:masterfrom
sankalpsthakur:agent/classical-mechanics-module-docs

Conversation

@sankalpsthakur

@sankalpsthakur sankalpsthakur commented Aug 2, 2026

Copy link
Copy Markdown
Contributor

Expands the Classical Mechanics module overview from a stub ("This file is currently a stub. Please feel free to contribute!") into a proper module documentation section following the library's # A, ## A.1/A.2/A.3 heading convention: scope of the module, current status (introduces no declarations itself), and future-work guidance for where shared vs. system-specific declarations belong.

Documentation only — no declarations, proofs, or signatures changed.

AI/LLM disclosure

AI coding tools were used to help draft this documentation. I reviewed the complete change for accuracy before submitting.

Co-authored-by: OpenAI GPT-5.6 Pro <noreply@openai.com>
@sankalpsthakur
sankalpsthakur marked this pull request as ready for review August 2, 2026 04:49
@github-actions

github-actions Bot commented Aug 2, 2026

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.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@github-actions github-actions Bot added the t-classical-mechanics Classical mechanics label Aug 2, 2026

@doxtor6 doxtor6 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. Again, It will be great if you can help to update the API-maps in the meanwhile. See details in https://github.com/jstoobysmith/PhyslibAITools

@doxtor6 doxtor6 added the ready-to-merge This PR is approved and will be merged shortly label Aug 2, 2026
@jstoobysmith

Copy link
Copy Markdown
Member

This is great! Many thanks for this first PR! Will merge this now

@jstoobysmith
jstoobysmith merged commit a78b5b0 into leanprover-community:master Aug 2, 2026
8 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 t-classical-mechanics Classical mechanics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants