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: apply pp_using_anonymous_constructor attribute #3735

Merged
merged 1 commit into from
Mar 22, 2024
Merged

feat: apply pp_using_anonymous_constructor attribute #3735

merged 1 commit into from
Mar 22, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Mar 21, 2024 •
edited
Loading

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.

@kmill kmill requested a review from kim-em as a code owner March 21, 2024 22:50
@kmill
feat: apply pp_using_anonymous_constructor attribute
fba9c03 
This attribute is applied to the following structures: `Sigma`, `PSigma`, `PProd`, `And`, `Subtype`, and `Fin`.
These were given this attribute in Lean 3.
@kmill kmill force-pushed the pp_using_anonymous_constructor_apply branch from 0b431f3 to fba9c03 Compare March 22, 2024 00:16
@kmill kmill enabled auto-merge March 22, 2024 00:16
@kmill kmill added this pull request to the merge queue Mar 22, 2024
@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 22, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d5701fc9123012615116f4dc3e093ea42d84de22 --onto 2c15cdda044e77bb8c3937c63501850790e60dc6. (2024-03-22 00:32:47)

Merged via the queue into leanprover:master with commit acb188f Mar 22, 2024
10 checks passed
@kmill kmill mentioned this pull request Mar 22, 2024
Merged
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.
2 participants
@kmill @leanprover-community-mathlib4-bot