Update type_classes.md

[Erotemic]

In https://lean-lang.org/theorem_proving_in_lean4/type_classes.html I noticed an error. In the 5th example part of it states:

#eval double (10 : Int)
-- 100

However, the actual evaluation returns 10 as-is. I'm not sure if this was meant to return 100 or 10 (the correct fix depends on the answer to that question), but assuming we really did want 100 there as a way to show how the resolution of Nat and Int are different, then this should be the correct patch.

[timotree3]

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