lean4-htt/tests/lean/interactive/hoverException.lean.expected.out
Leonardo de Moura 59acf01bc9 feat: relax auto-implicit restrictions
The new options `relaxedAutoBoundImplicitLocal` can be used to
disable this feature.

closes #1011
2022-02-08 12:17:42 -08:00

3 lines
104 B
Text

{"textDocument": {"uri": "file://hoverException.lean"},
"position": {"line": 2, "character": 14}}
null