Skip to content

fix: improve Name.isMetaprogramming#12767

Open
JovanGerb wants to merge 1 commit intoleanprover:masterfrom
JovanGerb:Jovan-isMetaprogramming
Open

fix: improve Name.isMetaprogramming#12767
JovanGerb wants to merge 1 commit intoleanprover:masterfrom
JovanGerb:Jovan-isMetaprogramming

Conversation

@JovanGerb
Copy link
Contributor

This PR makes sure that identifiers with Meta or Simproc in their name do not show up in library search results.

For example, Nat.Simproc.eq_add_gt can currently be suggested by library search, even though it is an implementation detail. Additionally, there are various declarations in mathlib in the Mathlib.Meta namespace that we do not want to suggest.

@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 Mar 3, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 3, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 145a12104887190a20b016f81c73810b25da3e91 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 00:35:48)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 145a12104887190a20b016f81c73810b25da3e91 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 12:46:49)

@leanprover-bot
Copy link
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 145a12104887190a20b016f81c73810b25da3e91 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-03 00:35:49)

@JovanGerb
Copy link
Contributor Author

changelog-language

@github-actions github-actions bot added the changelog-language Language features and metaprograms label Mar 3, 2026
@JovanGerb JovanGerb closed this Mar 3, 2026
@JovanGerb JovanGerb reopened this Mar 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms 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