Hover on by_contra! is not helpful

Stream: mathlib4

[Michael Stoll]

import Mathlib

example (x : ℤ) : x = 0 := by
  by_contra!
  sorry

Hovering over by_contra! just shows "this : ¬?m.45".
Replacing by by_contra and hovering gives the more extensive

¬?m.45

A hole (or placeholder term), which stands for an unknown term that is expected to be inferred based on context. For example, in @id _ Nat.zero, the _ must be the type of Nat.zero, which is Nat.

The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as unification.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:

    In match patterns, holes are catch-all patterns.
    In some tactics, such as refine' and apply, unsolved-for placeholders become new goals.

but which is also not really helpful when you want to know details on by_contra...

(I was trying to see if I can get by_contra! to use docs#not_and_or in place of docs#not_and in a situation where the goal is a conjunction.)

[Damiano Testa]

If you name the variable, you get the doc-string as a hover, which is probably what you were looking for.

[Damiano Testa]

I do not know why you do not get the doc-string when the identifier is missing, though.

[Eric Wieser]

This line is to blame

[Eric Wieser]

But if you name the variable, you still get a garbage hover if you hover over that variable

[Damiano Testa]

Eric Wieser said:

This line is to blame

Why is this?

[Eric Wieser]

It says "use this as the name, but pretend it came from by_contra!"

[Eric Wieser]

And so if you hover over by_contra!, you see what you'd see if you hovered over this in by_contra! this

[Eric Wieser]

Which, separately, is also broken

[Damiano Testa]

Ah, I see is the mkIdentFrom that messes the hover?

[Damiano Testa]

Indeed, replacing that line with

`(tactic| by_contra! $(mkIdent `this):ident $[: $ty]?)

makes the hover over by_contra! show the by_contra! doc-string.

[Eric Wieser]

Not providing a hover for the this binder is consistent with suffices

[Damiano Testa]

#24087