[Merged by Bors] - fix(Tactic/ToFun): correct location of hovers#39911

Closed

grunweg wants to merge 2 commits into

leanprover-community:masterfrom

grunweg:tofun-fixhovers

grunweg commented May 27, 2026 •

edited

Loading

Contributor

When an explicit name for the new declaration is given, make hovering over the to_fun keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

depends on: [Merged by Bors] - feat(Tactic/ToFun): warn if provided name matches autogenerated one #39598

grunweg added easy t-meta labels

github-actions Bot commented May 27, 2026 •

edited

Loading

PR summary 86fd8e4461

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

mathlib-dependent-issues Bot added the blocked-by-other-PR label

thorimur reviewed

View reviewed changes

Mathlib/Tactic/ToFun.lean Outdated


          fix(Tactic/ToFun): correct location of hovers

00cbee7

When an explicit name for the new declaration is given, ensure to make
hovering over the to_fun keyword show the keyword's documentation,
and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

grunweg force-pushed the tofun-fixhovers branch from 5edebcb to 00cbee7 Compare

May 28, 2026 09:41


          Update Mathlib/Tactic/ToFun.lean

86fd8e4

Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>

grunweg removed blocked-by-other-PR easy labels

mathlib-dependent-issues Bot commented May 28, 2026

This PR/issue depends on:

~~[Merged by Bors] - feat(Tactic/ToFun): warn if provided name matches autogenerated one #39598~~
By Dependent Issues (🤖). Happy coding!

thorimur commented May 28, 2026

Contributor

Thanks! :)

maintainer merge

github-actions Bot commented May 28, 2026

🚀 Pull request has been placed on the maintainer queue by thorimur.

mathlib-triage Bot added the maintainer-merge label

mathlib-triage Bot assigned dwrensha

adomani commented May 29, 2026

Contributor

Thanks!

bors merge

mathlib-triage Bot added ready-to-merge and removed maintainer-merge labels

mathlib-bors Bot pushed a commit that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (#39911)

c1c90fd

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

mathlib-bors Bot commented May 29, 2026

Contributor

Build failed (retrying...):

ci (staging) / Build

mathlib-bors Bot pushed a commit that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (#39911)

17fb0fd

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

mathlib-bors Bot commented May 29, 2026

Contributor

Build failed (retrying...):

ci (staging) / Build

mathlib-bors Bot pushed a commit that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (#39911)

3806c49

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

mathlib-bors Bot commented May 29, 2026

Contributor

Build failed (retrying...):

ci (staging) / Build

mathlib-bors Bot pushed a commit that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (#39911)

1a97b4b

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

mathlib-bors Bot commented May 29, 2026

Contributor

Build failed (retrying...):

ci (staging) / Build

mathlib-bors Bot pushed a commit that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (#39911)

15f13f4

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

mathlib-bors Bot commented May 29, 2026

Contributor

Pull request successfully merged into master.

Build succeeded:

mathlib-bors Bot changed the title ~~fix(Tactic/ToFun): correct location of hovers~~ [Merged by Bors] - fix(Tactic/ToFun): correct location of hovers

mathlib-bors Bot closed this

grunweg added a commit to grunweg/mathlib4 that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (leanprover-community#3…

5c67e3a

…9911)

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (leanprover-community#3…

4054e22

…9911)

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request


          fix(Tactic/ToFun): correct location of hovers (leanprover-community#3…

84f2e1b

…9911)

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge t-meta