Skip to content

Update type_classes.md #77

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

Open
Erotemic wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Update type_classes.md #77

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion type_classes.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ We can now reimplement `double` using an instance implicit by:
# instance : Add Nat where
# add := Nat.add
# instance : Add Int where
# add := Int.add
# add := Int.mul

@timotree3 timotree3 Oct 11, 2023

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These lines starting with # are hidden in the rendered book, and I assume they generally match code already shown earlier in the chapter. In the code block just above this one, this instance is defined to use Int.add, so readers would expect that definition here as well.

theorem_proving_in_lean4/type_classes.md

Lines 76 to 77 in 6643a27

instance : Add Int where
add := Int.add

I think what actually happened here is a copy-paste error from

#eval double { add := Nat.add } 10
-- 20

#eval double { add := Nat.mul } 10
-- 100

#eval double { add := Int.add } 10
-- 20

and since I don't see an easy way to keep the Nat.mul example without confusing the reader, I would recommend just changing 100 to 20

# instance : Add Float where
# add := Float.add
def double [Add a] (x : a) : a :=
Expand Down