Commit 2025-04-17 15:55 4a76948a

fix(ByContra hover): hover over by_contra! gets its doc-string back (#24087) Before this change, hovering over by_contra! showed this : ¬?m.45, i.e., the hover information coming from the implicit this. With this change, the hover information over by_contra! is the by_contra! doc-string string. The by_contra tactic from Batteries still suffers from a similar problem: the hover shows information about a hole, rather than the content of the by_contra doc-string. #mathlib4 > Hover on by_contra! is not helpful @ 💬