Skip to content

fix: getUsedConstants should record projection type names - #14728

Merged
Kha merged 1 commit into
masterfrom
hbv/fix_used_constants
Aug 10, 2026
Merged

fix: getUsedConstants should record projection type names#14728
Kha merged 1 commit into
masterfrom
hbv/fix_used_constants

Conversation

@hargoniX

@hargoniX hargoniX commented Aug 10, 2026

Copy link
Copy Markdown
Member

This PR makes Expr.getUsedConstants collect the typeName field of Expr.proj so we get a full list of constants that are directly used.

@hargoniX hargoniX added the changelog-library Library label Aug 10, 2026
@Kha
Kha enabled auto-merge August 10, 2026 08:45
@Kha
Kha added this pull request to the merge queue Aug 10, 2026
@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 10, 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 f7f5b4cda9b33387b512b84ea179461881b12500 --onto b1cd183c9978c3bedddc33baf7c9599baaeca046. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-10 09:09:18)

@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 f7f5b4cda9b33387b512b84ea179461881b12500 --onto b1cd183c9978c3bedddc33baf7c9599baaeca046. You can force reference manual CI using the force-manual-ci label. (2026-08-10 09:09:20)

Merged via the queue into master with commit 2315eae Aug 10, 2026
25 of 27 checks passed
@hargoniX
hargoniX deleted the hbv/fix_used_constants branch August 10, 2026 11:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library 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.

3 participants