commit: f8ccf5c6f7ef6c9137a3311dada62961e4943ce1

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Tue Oct 21 19:42:41 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Oct 21 19:44:08 2025 -0700
tree: c259c872fd75c240f456c694564e41a54dd5b4d2
parent: 38240612bc8ec04c8d98899e7862d75b93f263f0 [diff]

feat: use new `TermInfo.isDisplayableTerm` when hovering `grind` anchors

This PR uses the new `TermInfo.isDisplayableTerm` when hovering over
`cases` tactic anchors in the `grind` interactive mode.

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean[diff]

1 file changed

tree: c259c872fd75c240f456c694564e41a54dd5b4d2

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.