commit: b399b0912f6cc195f2859c1bea425c247772a45c

[log]
author: Kyle Miller <kmill31415@gmail.com>

Sat May 16 23:35:20 2026 -0700
committer: Kyle Miller <kmill31415@gmail.com>

Sat May 16 23:35:20 2026 -0700
tree: c4ab99f3439a9d0a99a59238dbfa31d27fd2519f
parent: 803553a556fd82fa1060efb0c43eda542130cb16 [diff]

feat: add `MessageData.withExprHover`

This PR adds `MessageData.withExprHover`, for creating messages that show information about an expression when hovered over. A `withExprHoverM` variant captures the current local context.

2 files changed

tree: c4ab99f3439a9d0a99a59238dbfa31d27fd2519f

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.