Skip to content

feat: add Repr instance for Vector - #14545

Open
Seasawher wants to merge 1 commit into
leanprover:masterfrom
Seasawher:vector-repr
Open

feat: add Repr instance for Vector#14545
Seasawher wants to merge 1 commit into
leanprover:masterfrom
Seasawher:vector-repr

Conversation

@Seasawher

@Seasawher Seasawher commented Jul 25, 2026

Copy link
Copy Markdown
Contributor

This PR renders Vector values using #v[...] literal notation instead of exposing their underlying structure representation, making evaluated vectors more concise and readable. It replaces the derived Repr instance.

see Zulip: #lean4 > Make the Repr instance for Vector to the literal notation

@Seasawher
Seasawher requested a review from kim-em as a code owner July 25, 2026 07:37
@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 Jul 25, 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 a2c74ef85a8212503551663871b90d0d51b7417f --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-25 08:00:56)

@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 a2c74ef85a8212503551663871b90d0d51b7417f --onto 156bdc91d998a1156341d899f43681190e74d2b8. You can force reference manual CI using the force-manual-ci label. (2026-07-25 08:00:57)

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