Skip to content

feat(naming): update naming conventions for Prop-valued classes#882

Open
fpvandoorn wants to merge 2 commits into
lean4from
IsHasNaming
Open

feat(naming): update naming conventions for Prop-valued classes#882
fpvandoorn wants to merge 2 commits into
lean4from
IsHasNaming

Conversation

@fpvandoorn

@fpvandoorn fpvandoorn commented Jun 22, 2026

Copy link
Copy Markdown
Member

@grunweg

grunweg commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

Thanks for the PR! Can you link to a Zulip discussion or similar where this was discussed?

@fpvandoorn

fpvandoorn commented Jun 22, 2026

Copy link
Copy Markdown
Member Author

It was discussed in-person in Institute Pascal after I made this comment: leanprover-community/mathlib4#40552 (comment)
Do small changes documenting existing practice (i.e. not asking to do anything new) require a Zulip discussion? (assuming this counts as "small")

@grunweg

grunweg commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

Ah, I see. But we have plenty of past discussions on Prop-valued classes, right --- was this also mentioned there? I trust you to make reasonable proposals, but I think "two people discuss something in person" is not a good group process, sorry. A brief post on Zulip and waiting for 24h seems better.

@fpvandoorn

fpvandoorn commented Jun 22, 2026

Copy link
Copy Markdown
Member Author

Sure, I was happy to wait for a few thumb ups here. But I now also posted a public message in an existing thread, which was probably required to get enough eyes on this anyway.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants