has_repr for `ulift`

Stream: general

[Yury G. Kudryashov]

Can we pretty print ulift.up x as up x, not { down := x} while printing other terms x : ulift α as x?

[Reid Barton]

(you're talking about the pretty-printer output, like in the tactic state view, right? is that really controlled by has_repr?)

[Yury G. Kudryashov]

Probably yes, and I wonder if it's clever enough to tell ulift.up x from anything else.

[Gabriel Ebner]

No those two are different.

[Yury G. Kudryashov]

What does has_repr control?

[Gabriel Ebner]

Does attribute [pp_using_anonymous_constructor] ulift help?

[Gabriel Ebner]

The has_repr instance controls what #eval ulift.up 42 prints.

[Yury G. Kudryashov]

And which function/class is responsible for #print/goals output?

[Eric Wieser]

Lean itself, I think

[Gabriel Ebner]

Yup: https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/pp.cpp

[Eric Wieser]

It sounds like we want a variant of the attribute that src#sigma has, pp_using_anonymous_constructor?

[Eric Wieser]

Perhaps pp_using_named_constructor? It would need to be added around here.

[Patrick Massot]

Note that the widget framework can also tweak how the tactic state is displayed. See the wonderful #5440 that sadly was never merged for ideological reasons.

[Eric Wieser]

In particular from #5440:

Even better, I'd prefer it implemented as part of the pretty-printer so it interacted right with pp options.

Having it only be part of widgets also stops it being used in error messages (although you could rightfully argue those should support widgets too)

[Reid Barton]

or by emacs users

[Johan Commelin]

... although you could rightfully argue emacs should support widgets too :wink:

[Reid Barton]

Sure, then at some point it comes down to organizational reasons like pretty-printing should be handled by the pretty-printer.

[Yury G. Kudryashov]

@Gabriel Ebner My actual use case is docs#opposite. I am separating multiplicative opposite from category theory opposite, and I'd like to define the former as

structure mul_opposite (α : Type*) : Type* := op :: (unop : α)

With pp_using_anonymous_constructor, it prints op x as ⟨x⟩. It would be nice to have op x instead. Currently I use

structure mul_opposite (α : Type*) : Type* := (unop : α)

postfix `ᵐᵒᵖ`:std.prec.max_plus := mul_opposite

namespace mul_opposite

def op : α → αᵐᵒᵖ := mk
@[simp] lemma mk_eq_op : (mk : α → αᵐᵒᵖ) = op := rfl

as a workaround.

[Gabriel Ebner]

I understand. It wouldn't be hard to implement (a pp_using_named_constructor attribute as Eric suggested sound like the best design), but I think the easiest approach here is to just wait for Lean 4.