Changelog

leanprover/lean4 · · 4 commits

MePo fix, hover API, and pp.universes cleanup

Fixes a MePo ranking bug, adds expression hover message helpers, and restores correct pretty-printing under `pp.universes`.

kmill kim-em thorimur

MePo was returning the worst premises (kim-em385efbb)

mepoSelector had a stale .reverse, so after MePo started returning suggestions in score-descending order it was accidentally taking the lowest-scoring premises instead of the best ones. This fixes the selector and adds a regression test to lock in the intended ordering.

New MessageData.withExprHover helpers (kmillce58140)

Lean now has a dedicated API for building message data that shows expression info on hover, plus a monadic variant that fills in the current local context automatically. This is a useful primitive for richer editor/documentation tooling and replaces ad hoc hover construction in tactic docs.

pp.universes no longer blocks non-universe constants (kmill43ef70d)

Pretty-printing now only disables unexpansion/dot-notation for constants when universe parameters are actually present, instead of treating all constants as affected by pp.universes. That restores expected output for things like ↔ and Nat.succ, and the added tests capture the regression.

Other misc changes

  • Removed the addInfo flag from elabSetOption and updated linter callers.
  • Added/adjusted tests for set_option info-tree handling.