Skip to content

Commit

Permalink
feat: hover / go-to-def for attribute cmd
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0
digama0 committed Apr 13, 2024
1 parent c24b419 commit c071b5c
Show file tree
Hide file tree
Showing 3 changed files with 89 additions and 78 deletions.
16 changes: 8 additions & 8 deletions src/Lean/Elab/Declaration.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -353,14 +353,14 @@ def elabMutual : CommandElab := fun stx => do
for builtin simprocs.
-/
let declNames ←
try
realizeGlobalConst ident
catch _ =>
let name := ident.getId.eraseMacroScopes
if (← Simp.isBuiltinSimproc name) then
pure [name]
else
throwUnknownConstant name
try
realizeGlobalConstWithInfos ident
catch _ =>
let name := ident.getId.eraseMacroScopes
if (← Simp.isBuiltinSimproc name) then
pure [name]
else
throwUnknownConstant name
let declName ← ensureNonAmbiguous ident declNames
Term.applyAttributes declName attrs
for attrName in toErase do
Expand Down
3 changes: 3 additions & 0 deletions tests/lean/interactive/hover.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,6 +229,9 @@ def my_intro : Nat := 1
--v textDocument/hover
example : α → α := by my_intro _; assumption

attribute [simp] my_intro
--^ textDocument/hover

example : Nat → True := by
intro x
--^ textDocument/hover
Expand Down
148 changes: 78 additions & 70 deletions tests/lean/interactive/hover.lean.expected.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -446,198 +446,206 @@
"end": {"line": 229, "character": 32}},
"contents": {"value": "my_intro tactic ", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 232, "character": 8}}
"position": {"line": 231, "character": 17}}
{"range":
{"start": {"line": 232, "character": 8}, "end": {"line": 232, "character": 9}},
{"start": {"line": 231, "character": 17},
"end": {"line": 231, "character": 25}},
"contents":
{"value": "```lean\nmy_intro : ℕ\n```\n***\nmy_intro term ",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 235, "character": 8}}
{"range":
{"start": {"line": 235, "character": 8}, "end": {"line": 235, "character": 9}},
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 235, "character": 4}}
"position": {"line": 238, "character": 4}}
{"range":
{"start": {"line": 235, "character": 2}, "end": {"line": 235, "character": 8}},
{"start": {"line": 238, "character": 2}, "end": {"line": 238, "character": 8}},
"contents":
{"value":
"The left hand side of an induction arm, `| foo a b c` or `| @foo a b c`\nwhere `foo` is a constructor of the inductive type and `a b c` are the arguments\nto the constructor.\n",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 238, "character": 4}}
"position": {"line": 241, "character": 4}}
{"range":
{"start": {"line": 238, "character": 2},
"end": {"line": 238, "character": 10}},
{"start": {"line": 241, "character": 2},
"end": {"line": 241, "character": 10}},
"contents":
{"value":
"The left hand side of an induction arm, `| foo a b c` or `| @foo a b c`\nwhere `foo` is a constructor of the inductive type and `a b c` are the arguments\nto the constructor.\n",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 238, "character": 9}}
"position": {"line": 241, "character": 9}}
{"range":
{"start": {"line": 238, "character": 9},
"end": {"line": 238, "character": 10}},
{"start": {"line": 241, "character": 9},
"end": {"line": 241, "character": 10}},
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 242, "character": 8}}
"position": {"line": 245, "character": 8}}
{"range":
{"start": {"line": 242, "character": 8}, "end": {"line": 242, "character": 9}},
{"start": {"line": 245, "character": 8}, "end": {"line": 245, "character": 9}},
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 244, "character": 12}}
"position": {"line": 247, "character": 12}}
{"range":
{"start": {"line": 244, "character": 12},
"end": {"line": 244, "character": 13}},
{"start": {"line": 247, "character": 12},
"end": {"line": 247, "character": 13}},
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 246, "character": 4}}
"position": {"line": 249, "character": 4}}
{"range":
{"start": {"line": 246, "character": 2}, "end": {"line": 246, "character": 8}},
{"start": {"line": 249, "character": 2}, "end": {"line": 249, "character": 8}},
"contents":
{"value":
"The left hand side of an induction arm, `| foo a b c` or `| @foo a b c`\nwhere `foo` is a constructor of the inductive type and `a b c` are the arguments\nto the constructor.\n",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 249, "character": 9}}
"position": {"line": 252, "character": 9}}
{"range":
{"start": {"line": 249, "character": 9},
"end": {"line": 249, "character": 10}},
{"start": {"line": 252, "character": 9},
"end": {"line": 252, "character": 10}},
"contents":
{"value":
"```lean\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 249, "character": 11}}
"position": {"line": 252, "character": 11}}
{"range":
{"start": {"line": 249, "character": 11},
"end": {"line": 249, "character": 13}},
{"start": {"line": 252, "character": 11},
"end": {"line": 252, "character": 13}},
"contents": {"value": "```lean\nih : True\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 254, "character": 6}}
"position": {"line": 257, "character": 6}}
{"range":
{"start": {"line": 254, "character": 4}, "end": {"line": 254, "character": 9}},
{"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}},
"contents":
{"value":
"```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 254, "character": 15}}
"position": {"line": 257, "character": 15}}
{"range":
{"start": {"line": 254, "character": 13},
"end": {"line": 254, "character": 18}},
{"start": {"line": 257, "character": 13},
"end": {"line": 257, "character": 18}},
"contents":
{"value":
"```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 257, "character": 6}}
"position": {"line": 260, "character": 6}}
{"range":
{"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}},
{"start": {"line": 260, "character": 4}, "end": {"line": 260, "character": 9}},
"contents":
{"value":
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 257, "character": 17}}
"position": {"line": 260, "character": 17}}
{"range":
{"start": {"line": 257, "character": 15},
"end": {"line": 257, "character": 20}},
{"start": {"line": 260, "character": 15},
"end": {"line": 260, "character": 20}},
"contents":
{"value":
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 260, "character": 27}}
"position": {"line": 263, "character": 27}}
{"range":
{"start": {"line": 260, "character": 27},
"end": {"line": 260, "character": 37}},
{"start": {"line": 263, "character": 27},
"end": {"line": 263, "character": 37}},
"contents":
{"value":
"```lean\nInhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α\n```\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 260, "character": 28}}
"position": {"line": 263, "character": 28}}
{"range":
{"start": {"line": 260, "character": 28},
"end": {"line": 260, "character": 36}},
{"start": {"line": 263, "character": 28},
"end": {"line": 263, "character": 36}},
"contents":
{"value":
"```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 266, "character": 2}}
"position": {"line": 269, "character": 2}}
{"range":
{"start": {"line": 266, "character": 2}, "end": {"line": 266, "character": 3}},
{"start": {"line": 269, "character": 2}, "end": {"line": 269, "character": 3}},
"contents":
{"value":
"```lean\nlet x :=\n match 0 with\n | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 269, "character": 4}}
"position": {"line": 272, "character": 4}}
{"range":
{"start": {"line": 269, "character": 4}, "end": {"line": 269, "character": 8}},
{"start": {"line": 272, "character": 4}, "end": {"line": 272, "character": 8}},
"contents":
{"value": "```lean\nauto (o : ℕ := by exact 1) : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 274, "character": 22}}
"position": {"line": 277, "character": 22}}
{"range":
{"start": {"line": 274, "character": 22},
"end": {"line": 274, "character": 23}},
{"start": {"line": 277, "character": 22},
"end": {"line": 277, "character": 23}},
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 274, "character": 13}}
"position": {"line": 277, "character": 13}}
{"range":
{"start": {"line": 274, "character": 13},
"end": {"line": 274, "character": 15}},
{"start": {"line": 277, "character": 13},
"end": {"line": 277, "character": 15}},
"contents": {"value": "```lean\n_e : 1 = x\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 279, "character": 8}}
"position": {"line": 282, "character": 8}}
{"range":
{"start": {"line": 279, "character": 8},
"end": {"line": 279, "character": 10}},
{"start": {"line": 282, "character": 8},
"end": {"line": 282, "character": 10}},
"contents": {"value": "```lean\n_e : 1 = 0\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 282, "character": 9}}
"position": {"line": 285, "character": 9}}
{"range":
{"start": {"line": 282, "character": 9},
"end": {"line": 282, "character": 10}},
{"start": {"line": 285, "character": 9},
"end": {"line": 285, "character": 10}},
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 287, "character": 13}}
"position": {"line": 290, "character": 13}}
{"range":
{"start": {"line": 287, "character": 13},
"end": {"line": 287, "character": 16}},
{"start": {"line": 290, "character": 13},
"end": {"line": 290, "character": 16}},
"contents":
{"value":
"```lean\nList.nil.{u} {α : Type u} : List α\n```\n***\n`[]` is the empty list. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 289, "character": 13}}
"position": {"line": 292, "character": 13}}
{"range":
{"start": {"line": 289, "character": 11},
"end": {"line": 289, "character": 15}},
{"start": {"line": 292, "character": 11},
"end": {"line": 292, "character": 15}},
"contents":
{"value":
"```lean\nList.cons.{u} {α : Type u} (head : α) (tail : List α) : List α\n```\n***\nIf `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the\nlist whose first element is `a` and with `l` as the rest of the list. \n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 291, "character": 18}}
"position": {"line": 294, "character": 18}}
{"range":
{"start": {"line": 291, "character": 17},
"end": {"line": 291, "character": 20}},
{"start": {"line": 294, "character": 17},
"end": {"line": 294, "character": 20}},
"contents":
{"value":
"```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List α → List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 294, "character": 26}}
"position": {"line": 297, "character": 26}}
{"range":
{"start": {"line": 294, "character": 25},
"end": {"line": 294, "character": 29}},
{"start": {"line": 297, "character": 25},
"end": {"line": 297, "character": 29}},
"contents":
{"value":
"```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 294, "character": 19}}
"position": {"line": 297, "character": 19}}
{"range":
{"start": {"line": 294, "character": 19},
"end": {"line": 294, "character": 22}},
{"start": {"line": 297, "character": 19},
"end": {"line": 297, "character": 22}},
"contents":
{"value":
"```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
Expand Down

0 comments on commit c071b5c

Please sign in to comment.