Skip to content

Conversation

adomasbaliuka
Copy link
Contributor

In line 164, (where I removed the redundant "a"), the placeholder is called y which has a different meaning from x. In line 128, the placeholder is also called x, which is in my opinion confusing.

@Julian Julian merged commit c407b65 into leanprover-community:master Aug 28, 2024
5 checks passed
@Julian
Copy link
Collaborator

Julian commented Aug 28, 2024

Thanks!

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