cf53db3b13
This PR fixes #12827, where hovering over `for` loop variables `x` and `h` in `for h : x in xs do` showed no type information in the new do elaborator. The fix adds `Term.addLocalVarInfo` calls for the loop variable and membership proof binder after they are introduced by `withLocalDeclsD` in `elabDoFor`. Closes #12827
7 lines
160 B
Text
7 lines
160 B
Text
set_option backward.do.legacy false
|
|
|
|
def test : IO Unit := do
|
|
for h : i in [1, 2, 3] do
|
|
--^ textDocument/hover
|
|
--^ textDocument/hover
|
|
pure ()
|