Skip to content

feat: introduce findMatchingDecl? for code quality checks wrapped in Lean.Linter (DRAFT) - #14880

Draft
wkrozowski wants to merge 1 commit into
leanprover:masterfrom
wkrozowski:wkr/findPosition
Draft

feat: introduce findMatchingDecl? for code quality checks wrapped in Lean.Linter (DRAFT)#14880
wkrozowski wants to merge 1 commit into
leanprover:masterfrom
wkrozowski:wkr/findPosition

Conversation

@wkrozowski

Copy link
Copy Markdown
Contributor

Read this section before submitting

  • Ensure your PR follows the External Contribution Guidelines.
  • Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
  • Include the link to your RFC or bug issue in the description.
  • 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.
  • For feat/fix PRs, the first paragraph starting with "This PR" must be present and will become a
    changelog entry unless the PR is labeled with no-changelog. If the PR does not have this label,
    it must instead be categorized with one of the changelog-* labels (which will be done by a
    reviewer for external PRs).
  • A toolchain of the form leanprover/lean4-pr-releases:pr-release-NNNN for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing release-ci on its own line.
  • If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
  • You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
  • Remove this section, up to and including the --- before submitting.

This PR <short changelog summary for feat/fix, see above>.

Closes <RFC or bug issue number fixed by this PR, if any>

@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 Aug 21, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 03d7a4efd5f74dc886ba33eab424611146d49e03 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 14:14:39)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 03d7a4efd5f74dc886ba33eab424611146d49e03 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 14:14:40)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants