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

feat: show decl module in hover

Browse source
This commit is contained in:
Mario Carneiro 2022-09-23 12:09:10 -04:00 • committed by Leonardo de Moura
parent 121b18f40a
commit 5644bd7a3f
5 changed files with 48 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/Lean/Server/InfoUtils.lean
View file

@ -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

8
tests/lean/interactive/catHover.lean.expected.out
View file

@ -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"}}

34
tests/lean/interactive/hover.lean.expected.out
View file

@ -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}}

8
tests/lean/interactive/hoverDot.lean.expected.out
View file

@ -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"}}

10
tests/lean/interactive/lean3HoverIssue.lean.expected.out
View file

@ -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"}}