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.

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

chore: update changelog #2254

Closed
wants to merge 1 commit into from
Closed

chore: update changelog #2254

wants to merge 1 commit into from

Conversation

digama0
Copy link
Collaborator

@digama0 digama0 commented Jun 2, 2023

Add an entry for #2247. I elected not to mention either of the two main features actually implemented (have _ and the hygieneInfo matcher) because they are of a more technical nature. The more user-visible effect is the unkeywordification of this.

@Kha
Copy link
Member

Kha commented Jun 2, 2023

My bad, presented like this it does sound like a straight bugfix, which we don't usually document. I was thinking about the changed scoping behavior of this, but it seems quite unlikely that anyone made use of it across macro scopes in a way that would now break. What do you think?

@Kha
Copy link
Member

Kha commented Jun 2, 2023

Or perhaps more succinctly: "this is now an identifier again that is implicitly introduced by anonymous have := with regular scoping. It used to be a keyword that was visible in all scopes and led to unexpected behavior when explicitly used as a binder name.

@digama0
Copy link
Collaborator Author

digama0 commented Jun 2, 2023

I was thinking about the changed scoping behavior of this, but it seems quite unlikely that anyone made use of it across macro scopes in a way that would now break. What do you think?

I don't think anyone has used this in a macro, at least not that I have seen in mathlib and certainly not in the two or more nested macro-macros case that would actually be affected by this.

I am fine with your rewording. I was probably too hard on the original version so it is probably best for you to phrase it.

@Kha Kha closed this in af6c7cd Jun 3, 2023
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.

2 participants