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
10 lines
521 B
Text
10 lines
521 B
Text
{"textDocument": {"uri": "file:///hoverDoForIn.lean"},
|
|
"position": {"line": 3, "character": 6}}
|
|
{"range":
|
|
{"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}},
|
|
"contents": {"value": "```lean\nh : i ∈ [1, 2, 3]\n```", "kind": "markdown"}}
|
|
{"textDocument": {"uri": "file:///hoverDoForIn.lean"},
|
|
"position": {"line": 3, "character": 10}}
|
|
{"range":
|
|
{"start": {"line": 3, "character": 10}, "end": {"line": 3, "character": 11}},
|
|
"contents": {"value": "```lean\ni : Nat\n```", "kind": "markdown"}}
|