max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: for Lean 3 hover issue reported on Zulip

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-02 15:21:24 -07:00
parent 4fa5f50559
commit 78007be772
2 changed files with 57 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/interactive/lean3HoverIssue.lean Normal file
View file

@ -0,0 +1,12 @@
example (x y : Nat) (h : x = y) : y = x := by exact h.symm
--^ textDocument/hover
--^ textDocument/hover
example (x y : Nat) (h : x = y) : y = x := h.symm
--^ textDocument/hover
example (x y : Nat) (h : x = y) : y = x := by exact (Eq.symm (Eq.symm h.symm))
--^ textDocument/hover
--^ textDocument/hover
--^ textDocument/hover
--^ textDocument/hover

45
tests/lean/interactive/lean3HoverIssue.lean.expected.out Normal file
View file

@ -0,0 +1,45 @@
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 0, "character": 55}}
{"range":
{"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}},
"contents":
{"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 0, "character": 52}}
{"range":
{"start": {"line": 0, "character": 52}, "end": {"line": 0, "character": 53}},
"contents": {"value": "```lean\nh : x = y\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 4, "character": 46}}
{"range":
{"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}},
"contents":
{"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 7, "character": 54}}
{"range":
{"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}},
"contents":
{"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 7, "character": 65}}
{"range":
{"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}},
"contents":
{"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 7, "character": 70}}
{"range":
{"start": {"line": 7, "character": 70}, "end": {"line": 7, "character": 71}},
"contents": {"value": "```lean\nh : x = y\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
"position": {"line": 7, "character": 72}}
{"range":
{"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}},
"contents":
{"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
"kind": "markdown"}}