Skip to content

fix: warn on deprecated fields in structure instances - #15225

Draft
skwh54 wants to merge 1 commit into
leanprover:masterfrom
skwh54:fix/struct-field-deprecation
Draft

skwh54 wants to merge 1 commit into
leanprover:masterfrom
skwh54:fix/struct-field-deprecation

Conversation

@skwh54

@skwh54 skwh54 commented Sep 19, 2026

Copy link
Copy Markdown

This PR adds deprecation warnings for explicitly assigned structure and class fields, including inherited fields and parent projections.
Omitted defaults and copied fields do not trigger warnings, and existing deprecation suppression still applies.

findParentProjInfo? replaces findParentProjStruct? and returns the matched StructureParentInfo so the elaborator can check the correct projection. Regression tests cover nested updates, suppression, and parent projection selection.

Closes #15203.

Generative AI assistance: AI was used to assist with implementation and regression tests.

@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 Sep 19, 2026

This branch has not been deployed

No deployments
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.

@[deprecated] on a structure field projection does not warn when constructing the field

1 participant