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.
In https://lean-lang.org/theorem_proving_in_lean4/type_classes.html I noticed an error. In the 5th example part of it states:
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.