From 5644bd7a3faf1e8ddc4bf5b6060baefc431bf2e1 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 23 Sep 2022 12:09:10 -0400 Subject: [PATCH] feat: show decl module in hover --- src/Lean/Server/InfoUtils.lean | 32 +++++++++-------- .../interactive/catHover.lean.expected.out | 8 ++--- .../lean/interactive/hover.lean.expected.out | 34 ++++++++++--------- .../interactive/hoverDot.lean.expected.out | 8 ++--- .../lean3HoverIssue.lean.expected.out | 10 +++--- 5 files changed, 48 insertions(+), 44 deletions(-) diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index c8c55eae4e..b7f453b093 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -186,33 +186,39 @@ def Info.docString? (i : Info) : MetaM (Option String) := do def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do ci.runMetaM i.lctx do let mut fmts := #[] - try - if let some f ← fmtTerm? then + let modFmt ← try + let (termFmt, modFmt) ← fmtTermAndModule? + if let some f := termFmt then fmts := fmts.push f - catch _ => pure () + pure modFmt + catch _ => pure none if let some m ← i.docString? then fmts := fmts.push m + if let some f := modFmt then + fmts := fmts.push f if fmts.isEmpty then return none else return f!"\n***\n".joinSep fmts.toList where - fmtTerm? : MetaM (Option Format) := do + fmtModule? (decl : Name) : MetaM (Option Format) := do + let some mod ← findModuleOf? decl | return none + return some f!"*import {mod}*" + + fmtTermAndModule? : MetaM (Option Format × Option Format) := do match i with | Info.ofTermInfo ti => let e ← instantiateMVars ti.expr if e.isSort then -- Types of sorts are funny to look at in widgets, but ultimately not very helpful - return none + return (none, none) let tp ← instantiateMVars (← Meta.inferType e) let tpFmt ← Meta.ppExpr tp if e.isConst then -- Recall that `ppExpr` adds a `@` if the constant has implicit arguments, and it is quite distracting let eFmt ← withOptions (pp.fullNames.set · true |> (pp.universes.set · true)) <| PrettyPrinter.ppConst e - return some f!"```lean -{eFmt} : {tpFmt} -```" + return (some f!"```lean\n{eFmt} : {tpFmt}\n```", ← fmtModule? e.constName!) else let eFmt ← Meta.ppExpr e -- Try not to show too scary internals @@ -222,16 +228,12 @@ where else false else isAtomicFormat eFmt let fmt := if showTerm then f!"{eFmt} : {tpFmt}" else tpFmt - return some f!"```lean -{fmt} -```" + return (some f!"```lean\n{fmt}\n```", none) | Info.ofFieldInfo fi => let tp ← Meta.inferType fi.val let tpFmt ← Meta.ppExpr tp - return some f!"```lean -{fi.fieldName} : {tpFmt} -```" - | _ => return none + return (some f!"```lean\n{fi.fieldName} : {tpFmt}\n```", none) + | _ => return (none, none) isAtomicFormat : Format → Bool | Std.Format.text _ => true diff --git a/tests/lean/interactive/catHover.lean.expected.out b/tests/lean/interactive/catHover.lean.expected.out index e68f0d5aae..1b3f3d24e9 100644 --- a/tests/lean/interactive/catHover.lean.expected.out +++ b/tests/lean/interactive/catHover.lean.expected.out @@ -4,7 +4,7 @@ {"start": {"line": 4, "character": 32}, "end": {"line": 4, "character": 36}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://catHover.lean"}, "position": {"line": 4, "character": 14}} @@ -12,7 +12,7 @@ {"start": {"line": 4, "character": 14}, "end": {"line": 4, "character": 18}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://catHover.lean"}, "position": {"line": 4, "character": 25}} @@ -36,7 +36,7 @@ {"start": {"line": 17, "character": 15}, "end": {"line": 17, "character": 19}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://catHover.lean"}, "position": {"line": 20, "character": 9}} @@ -44,5 +44,5 @@ {"start": {"line": 20, "character": 7}, "end": {"line": 20, "character": 11}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index e02b5a479a..bdf2a76f29 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -4,7 +4,7 @@ {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 18}}, "contents": {"value": - "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", + "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 7, "character": 8}} @@ -12,7 +12,7 @@ {"start": {"line": 7, "character": 8}, "end": {"line": 7, "character": 18}}, "contents": {"value": - "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", + "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 12, "character": 4}} @@ -20,7 +20,7 @@ {"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}}, "contents": {"value": - "```lean\nNat.zero : Nat\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. ", + "```lean\nNat.zero : Nat\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": 21, "character": 2}} @@ -38,7 +38,7 @@ {"start": {"line": 21, "character": 13}, "end": {"line": 21, "character": 23}}, "contents": {"value": - "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", + "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 28, "character": 6}} @@ -46,7 +46,7 @@ {"start": {"line": 28, "character": 6}, "end": {"line": 28, "character": 12}}, "contents": {"value": - "```lean\nLean.Parser.Category.tactic : Lean.Parser.Category\n```\n***\n`tactic` is the builtin syntax category for tactics. These appear after\n`by` in proofs, and they are programs that take in the proof context\n(the hypotheses in scope plus the type of the term to synthesize) and construct\na term of the expected type. For example, `simp` is a tactic, used in:\n```\nexample : 2 + 2 = 4 := by simp\n```\n", + "```lean\nLean.Parser.Category.tactic : Lean.Parser.Category\n```\n***\n`tactic` is the builtin syntax category for tactics. These appear after\n`by` in proofs, and they are programs that take in the proof context\n(the hypotheses in scope plus the type of the term to synthesize) and construct\na term of the expected type. For example, `simp` is a tactic, used in:\n```\nexample : 2 + 2 = 4 := by simp\n```\n\n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 28, "character": 32}} @@ -54,7 +54,7 @@ {"start": {"line": 28, "character": 32}, "end": {"line": 28, "character": 36}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 31, "character": 6}} @@ -62,7 +62,7 @@ {"start": {"line": 31, "character": 6}, "end": {"line": 31, "character": 12}}, "contents": {"value": - "```lean\nLean.Parser.Category.tactic : Lean.Parser.Category\n```\n***\n`tactic` is the builtin syntax category for tactics. These appear after\n`by` in proofs, and they are programs that take in the proof context\n(the hypotheses in scope plus the type of the term to synthesize) and construct\na term of the expected type. For example, `simp` is a tactic, used in:\n```\nexample : 2 + 2 = 4 := by simp\n```\n", + "```lean\nLean.Parser.Category.tactic : Lean.Parser.Category\n```\n***\n`tactic` is the builtin syntax category for tactics. These appear after\n`by` in proofs, and they are programs that take in the proof context\n(the hypotheses in scope plus the type of the term to synthesize) and construct\na term of the expected type. For example, `simp` is a tactic, used in:\n```\nexample : 2 + 2 = 4 := by simp\n```\n\n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 31, "character": 24}} @@ -70,7 +70,7 @@ {"start": {"line": 31, "character": 23}, "end": {"line": 31, "character": 27}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 36, "character": 2}} @@ -120,7 +120,7 @@ {"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}}, "contents": {"value": - "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n", + "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 77, "character": 10}} @@ -136,21 +136,23 @@ {"start": {"line": 82, "character": 7}, "end": {"line": 82, "character": 8}}, "contents": {"value": - "```lean\nNat : Type\n```\n***\nThe type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n", + "```lean\nNat : Type\n```\n***\nThe type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 87, "character": 14}} {"range": {"start": {"line": 87, "character": 14}, "end": {"line": 87, "character": 36}}, "contents": - {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```", + {"value": + "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```\n***\n*import Lean.Parser.Do*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 89, "character": 30}} {"range": {"start": {"line": 89, "character": 29}, "end": {"line": 89, "character": 34}}, "contents": - {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```", + {"value": + "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```\n***\n*import Lean.Parser.Do*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 92, "character": 2}} @@ -169,7 +171,7 @@ "end": {"line": 102, "character": 23}}, "contents": {"value": - "```lean\nLean.Parser.ppSpace : Lean.Parser.Parser\n```\n***\nNo-op parser that advises the pretty printer to emit a space/soft line break. ", + "```lean\nLean.Parser.ppSpace : Lean.Parser.Parser\n```\n***\nNo-op parser that advises the pretty printer to emit a space/soft line break. \n***\n*import Lean.Parser.Extra*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 102, "character": 24}} @@ -178,7 +180,7 @@ "end": {"line": 102, "character": 31}}, "contents": {"value": - "```lean\nLean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. ", + "```lean\nLean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 102, "character": 31}} @@ -187,7 +189,7 @@ "end": {"line": 102, "character": 35}}, "contents": {"value": - "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 111, "character": 2}} @@ -210,7 +212,7 @@ "end": {"line": 119, "character": 10}}, "contents": {"value": - "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n", + "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 119, "character": 10}} diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index 3b904e4b76..b7b8d13761 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -19,7 +19,7 @@ {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}}, "contents": {"value": - "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. ", + "```lean\nNat.succ : Nat → Nat\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://hoverDot.lean"}, "position": {"line": 16, "character": 11}} @@ -32,7 +32,7 @@ {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}}, "contents": {"value": - "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. ", + "```lean\nNat.succ : Nat → Nat\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://hoverDot.lean"}, "position": {"line": 19, "character": 13}} @@ -45,7 +45,7 @@ {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}}, "contents": {"value": - "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. ", + "```lean\nNat.succ : Nat → Nat\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://hoverDot.lean"}, "position": {"line": 22, "character": 14}} @@ -58,5 +58,5 @@ {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}}, "contents": {"value": - "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. ", + "```lean\nNat.succ : Nat → Nat\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"}} diff --git a/tests/lean/interactive/lean3HoverIssue.lean.expected.out b/tests/lean/interactive/lean3HoverIssue.lean.expected.out index e3184a3192..8d10618c6b 100644 --- a/tests/lean/interactive/lean3HoverIssue.lean.expected.out +++ b/tests/lean/interactive/lean3HoverIssue.lean.expected.out @@ -4,7 +4,7 @@ {"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 0, "character": 52}} @@ -17,7 +17,7 @@ {"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 7, "character": 54}} @@ -25,7 +25,7 @@ {"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 7, "character": 65}} @@ -33,7 +33,7 @@ {"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 7, "character": 70}} @@ -46,5 +46,5 @@ {"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}}