theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
Update type_classes.md
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.