custom representation in goal view

Stream: new members

[Horatiu Cheval]

Is there a way to change the way terms are shown in the goal view with a custom representation? Like what has_repr does for #eval, but for the goal view

[Eric Wieser]

If there were, it would have to operate on exprs and not terms of that type

[Eric Wieser]

Do you have an example of what you hope to use this for? Maybe the Rubik's cube and Hanoi widget examples are close to what you're hoping for.

[Horatiu Cheval]

I didn't know those project, I'll check them out. My problem is essentially that I don't understand how notation works with the infoview. Sometimes terms are printed in the custom notation I define, while other times the notation gets unfolded into a rather unreadable term which the custom notation shouls stand for. I would like the infoview to always show these terms using the notation I define and I don't know how to achieve that.

[Eric Wieser]

I think what you're referring to is what lean4 calls a "deelaborator", and lean3 doesn't have them