Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: move docstrings for open, variable, universe, export from elaborator to parser #3891

Merged
merged 1 commit into from
Apr 17, 2024

Conversation

TwoFX
Copy link
Member

@TwoFX TwoFX commented Apr 12, 2024

During the documentation sprint we discussed that user-visible documentation for syntax should generally go on the parser instead of the elaborator.

@TwoFX TwoFX added the documentation Documentation improvement label Apr 12, 2024
@TwoFX TwoFX requested a review from Kha as a code owner April 12, 2024 16:40
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 12, 2024 16:54 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 12, 2024
@TwoFX TwoFX added the will-merge-soon …unless someone speaks up label Apr 16, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 16, 2024 07:41 Inactive
@TwoFX TwoFX added this pull request to the merge queue Apr 17, 2024
Merged via the queue into master with commit d3e0049 Apr 17, 2024
19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Documentation improvement toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants