`for ... in ...` do elaborator doesn't produce term info

[Rob23oba]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The for x in y and for h : x in y do elaborator don't produce any term info for x or h, i.e. they are not highlighted and hovering on them doesn't show information about them.

Context

Trying out the new do elaborator.

Steps to Reproduce

set_option backward.do.legacy false

def test : IO Unit := do
  for h : i in [1, 2, 3] do -- Try hovering over `h` and `i`
    pure ()

Expected behavior:
Hovering over h shows h : i ∈ [1, 2, 3] and hovering over i shows i : Nat.

Actual behavior:
Hovering only shows the documentation of the for ... in ... elaborator and the result type IO Unit.

Versions

Lean 4.30.0-nightly-2026-03-05

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.