[Merged by Bors] - fix(meta/expr): adjust is_likely_generated_binder_name to lean#490 #4915
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts `name.is_likely_generated_binder_name`, which checks whether a binder name was likely generated by Lean (rather than given by the user).
|
@gebner could you take a look at this? Particularly whether the docs are still accurate. |
eric-wieser
approved these changes
Nov 5, 2020
|
Do you mind adding a test so that we'll remember this if we change the name again in the future? |
bryangingechen
added
awaiting-review
|
I agree with Bryan, this deserves a test. bors d+ |
|
✌️ JLimperg can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
delegated
|
Added the test case. Thanks for the suggestion and reviews everyone! bors r+ |
bors bot
pushed a commit
that referenced
this pull request
Nov 6, 2020
…4915) Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts `name.is_likely_generated_binder_name`, which checks whether a binder name was likely generated by Lean (rather than given by the user).
|
Build failed: |
|
The build failure seems to be caused by the problem discussed in this Zulip thread. Retrying... bors r+ |
bors bot
pushed a commit
that referenced
this pull request
Nov 6, 2020
…4915) Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts `name.is_likely_generated_binder_name`, which checks whether a binder name was likely generated by Lean (rather than given by the user).
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Nov 6, 2020
…4915) Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts `name.is_likely_generated_binder_name`, which checks whether a binder name was likely generated by Lean (rather than given by the user).
|
Build failed: |
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Nov 6, 2020
…4915) Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts `name.is_likely_generated_binder_name`, which checks whether a binder name was likely generated by Lean (rather than given by the user).
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
b-mehta
pushed a commit
that referenced
this pull request
Nov 12, 2020
…4915) Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts `name.is_likely_generated_binder_name`, which checks whether a binder name was likely generated by Lean (rather than given by the user).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Lean PR 490 changed Lean's strategy for generating binder names. This PR adapts
name.is_likely_generated_binder_name, which checks whether a binder name waslikely generated by Lean (rather than given by the user).