Skip to content

I integrated Violetta's highlights manually. #846

Open
bigmac0 wants to merge 14 commits into
leanprover:mainfrom
bigmac0:bigmac0-highlights
Open

I integrated Violetta's highlights manually. #846
bigmac0 wants to merge 14 commits into
leanprover:mainfrom
bigmac0:bigmac0-highlights

Conversation

@bigmac0
Copy link
Copy Markdown

@bigmac0 bigmac0 commented May 7, 2026

Read this section before submitting

  • Ensure your PR follows the External Contribution Guidelines.
  • Help your PR get merged quickly by making it fast to review:
    • Please open multiple pull requests to fix multiple small issues
    • Don't make systematic changes to English usage without discussing them first
    • Don't submit large amounts of new content without discussing it first
  • If the issue does not already have approval from a developer, submit the PR as draft.
  • The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
  • Remove this section, up to and including the --- before submitting.

Closes #0000 (issue number fixed by this PR, if any)

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.

2 participants