lean4-htt

40408 commits 1 branch 0 tags 5.3 GiB

Author SHA1 Message Date

Author	SHA1	Message	Date
Joachim Breitner	9151360469	fix: preserve symbol hover for `fun_induction` function target (#13678 ) This PR ensures that one can hover over the function name in fun_induction. Fixes #13673 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>	2026-05-07 12:09:36 +00:00
Garmelon	a3cb39eac9	chore: migrate more tests to new test suite (#12809 ) This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.	2026-03-06 16:52:01 +00:00

Joachim Breitner

9151360469

fix: preserve symbol hover for fun_induction function target (#13678 )

This PR ensures that one can hover over the function name in
fun_induction. Fixes #13673

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

2026-05-07 12:09:36 +00:00

Garmelon

a3cb39eac9

chore: migrate more tests to new test suite (#12809 )

This PR migrates most remaining tests to the new test suite. It also
completes the migration of directories like `tests/lean/run`, meaning
that PRs trying to add tests to those old directories will now fail.

2026-03-06 16:52:01 +00:00

Renamed from tests/lean/interactive/hover.lean (Browse further)

2 commits