Zulip Chat Archive
Stream: mathlib4
Topic: ambiguous identifier
Johan Commelin (Jun 05 2023 at 12:37):
ambiguous identifier 'eapproxDiff', possible interpretations: [SimpleFunc.eapproxDiff, SimpleFunc.eapproxDiff]
No kidding...
Mario Carneiro (Jun 05 2023 at 14:12):
have you tried using SimpleFunc.eapproxDiff?
Damiano Testa (Jun 05 2023 at 14:13):
... or SimpleFunc.eapproxDiff, if Mario's suggestion does not work?
Johan Commelin (Jun 05 2023 at 14:41):
I tried both! At least one of them worked, but I couldn't figure out which one.
Damiano Testa (Jun 05 2023 at 14:49):
If only mathlib were classical, we could conclude that you accomplished your goals.
Last updated: Dec 20 2023 at 11:08 UTC