Infoview `abbrev`

Stream: lean4

[Martin Dvořák]

Can I make Infoview respect abbrev (i.e., show the LHS (shorter version) term)?

[Eric Wieser]

You can maybe rw [← yourAbbrev]

[Yaël Dillies]

That sadly doesn't work.

[Martin Dvořák]

I guess we have a case for reducible def over abbrev now.

[Eric Wieser]

Do you have a #mwe where they're different?

[Martin Dvořák]

I can make it, but the difference is in the Infoview, not in the code.

[Eric Wieser]

If the infoview reproduces from the mwe, then that's all that matters

[François G. Dorais]

abbrev doesn't generate the same equation lemmas, which is why the rw doesn't work. I feel into a similar trap this morning where a function got marked noncomputable because it was matching on a term that was an abbrev instead of a @[reducible] def.

[Martin Dvořák]

Martin Dvořák said:

I can make it, but the difference is in the Infoview, not in the code.

I cannot replicate it now. I think I just overlooked something previously.
Consider my comment to be wrong and continue with the original topic if there is something to say about it.