Zulip Chat Archive
Stream: lean4
Topic: Diff of mismatching types
Pedro Sánchez Terraf (Dec 29 2023 at 14:28):
This is a feature request, but perhaps I'm asking for an already existing capability.
I'd like that one could have colored diffs in Infoview when you have a type mismatch error. Sometimes (at least for me) I have two types that are almost the same but with just few differences that are to difficult to find at a glance.
If this doesn't exist already, would anyone else find it useful? (Disclaimer: I do not know how to implement such an extension of the VSCode extension).
Kyle Miller (Dec 29 2023 at 14:38):
It would be nice if it could adjust how things pretty print so that you can see differences in implicit arguments
Kyle Miller (Dec 29 2023 at 15:14):
Want to create a Lean 4 issue with a feature request for expected type diffing? (After checking there isn't already one?)
Pedro Sánchez Terraf (Dec 29 2023 at 15:22):
Oh ok, and also after I figure out how do I do that :sweat_smile:. I guess that seeing
previous examples would be enough.
PST.-
—sent from mobile
El vie, 29 de dic de 2023, 12:16, Zulip notifications <noreply@zulip.com>
escribió:
Eric Wieser (Dec 29 2023 at 15:32):
The mechanism for this already exists, as we already use it for showing diffs in the info view evolution, right?
Damiano Testa (Dec 29 2023 at 15:46):
I think that it used to be Widget.exprDiff, but I cannot find it anymore...
Damiano Testa (Dec 29 2023 at 15:47):
... or maybe docs#Lean.Widget.exprDiff ?
Pedro Sánchez Terraf (Jan 02 2024 at 12:59):
Hope it was presented clearly enough!
Last updated: May 02 2025 at 03:31 UTC