Skip to content

fix: expose Vector DecidableEq for kernel reduction - #14988

Open
kim-em wants to merge 1 commit into
leanprover:masterfrom
kim-em:expose-vector-decidableeq
Open

fix: expose Vector DecidableEq for kernel reduction#14988
kim-em wants to merge 1 commit into
leanprover:masterfrom
kim-em:expose-vector-decidableeq

Conversation

@kim-em

@kim-em kim-em commented Sep 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

This PR lets the derived Vector DecidableEq instance reduce in the kernel across module boundaries.

Opt Vector into the supported per-derivation @[expose] annotation while leaving derived instances opaque by default. The regression uses an empty vector so it isolates the generated decEq helper and does not depend on exposing nonempty Array equality.

Split from the original #14270 alongside the independent Array.ofFn fix in #14989.

@kim-em
fix: expose Vector DecidableEq for kernel reduction
5180276 
Opt the derived Vector DecidableEq helper into exposure so decide and rfl reduce across module boundaries while other derived instances remain opaque by default.
This was referenced Sep 1, 2026
Draft
Open
@kim-em kim-em added the changelog-language Language features and metaprograms label Sep 1, 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 Sep 1, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Sep 1, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-09-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-01 14:12:30)

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 1, 2026
@leanprover-bot

leanprover-bot commented Sep 1, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

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

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR 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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em @leanprover-bot