ambiguous overload, possible interpretations
2 + 2
2 + 2
Additional information:
/home/joe/theorem_proving_in_lean_examples/10_3.lean:17:9: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
Without the type hinting I got:
ambiguous overload, possible interpretations 2 + 2 2 + 2 Additional information: /home/joe/theorem_proving_in_lean_examples/10_3.lean:17:9: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available