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

[Typo] Extra word in section 8.5 #164

Open
mars0i opened this issue Oct 3, 2024 · 1 comment
Open

[Typo] Extra word in section 8.5 #164

mars0i opened this issue Oct 3, 2024 · 1 comment
Labels
Typo Typographical or grammatical errors in the text

Comments

@mars0i
Copy link

mars0i commented Oct 3, 2024

Section 8.5 "Instead, Lean considers functions to be definitionally equal either when they are both fun-expressions with definitionally equal bodies."

The word "either" should be deleted.
@mars0i mars0i added the Typo Typographical or grammatical errors in the text label Oct 3, 2024
@mars0i mars0i changed the title [Typo] [Typo] Extra word in section 8.5 Oct 3, 2024
@MoSa89
Copy link

MoSa89 commented Oct 8, 2024

May I fix it?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Typo Typographical or grammatical errors in the text
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mars0i @MoSa89