Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add pp_using_anonymous_constructor attribute #3640

Merged
merged 1 commit into from
Mar 21, 2024
Merged

feat: add pp_using_anonymous_constructor attribute #3640

merged 1 commit into from
Mar 21, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Mar 9, 2024 •
edited
Loading

Implements a Lean 3 pretty printer feature. Structures with the @[pp_using_anonymous_constructor] attribute pretty using anonymous constructor notation (⟨x, y, z⟩) rather than structure instance notation ({a := x, b := y, c := z}).

Zulip discussion

@kmill kmill requested a review from kim-em as a code owner March 9, 2024 17:36
@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 9, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 9, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-09 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-09 17:55:02)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 085d01942d5bfea2461b9fab95438a4c2ed1b56d --onto 2c15cdda044e77bb8c3937c63501850790e60dc6. (2024-03-21 23:03:05)

@kmill kmill force-pushed the pp_using_anonymous_constructor branch from 0ecd1b6 to 117b98c Compare March 21, 2024 22:41
@kmill kmill changed the title feat: define pp_using_anonymous_constructor attribute and apply it feat: add pp_using_anonymous_constructor attribute Mar 21, 2024
@kmill
feat: add pp_using_anonymous_constructor attribute
09ac94c 
This attribute causes structures to pretty print
using anonymous constructor notation (`⟨x, y, z⟩`)
rather than structure instance notation (`{a := x, b := y, c := z}`).
@kmill kmill force-pushed the pp_using_anonymous_constructor branch from 117b98c to 09ac94c Compare March 21, 2024 22:45
@kmill kmill enabled auto-merge March 21, 2024 22:46
@kmill kmill added this pull request to the merge queue Mar 21, 2024
@kmill kmill mentioned this pull request Mar 21, 2024
Merged
Merged via the queue into leanprover:master with commit ff7a0db Mar 21, 2024
10 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Mar 22, 2024
@kmill
feat: apply pp_using_anonymous_constructor attribute (#3735)
acb188f 
This attribute, which was implemented in #3640, is applied to the
following structures: `Sigma`, `PSigma`, `PProd`, `And`, `Subtype`, and
`Fin`. These were given this attribute in Lean 3.
@nomeata
Copy link
Collaborator

nomeata commented Mar 22, 2024

Thanks a lot! Pretty please enable this for PProd, it'll make my life dealing with well-founded recursion so much better :-)

@kmill
Copy link
Collaborator Author

kmill commented Mar 22, 2024

@nomeata It's already been done in #3735 😃 (this needed a stage0 update first)

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

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
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.
3 participants
@kmill @leanprover-community-mathlib4-bot @nomeata