2ede81fe10
This PR fixes a number of bugs related to the handling of the source search path in the language server, where deleting files could cause several features to stop functioning and both untitled files and files that don't exist on disc could have conflicting module names. In detail, it makes the following adjustments: - The URI <-> module name conversion was adjusted to produce no name collisions. - File URIs in the search path yield a module name relative to the search path, as before. - File URIs not in the search path, non-file URIs and non-`.lean` files yield a `«external:<full uri>»` module name. - To avoid the issue of the URI -> module name conversion failing when a file is deleted from disc, we now cache the result of this conversion in the watchdog and the file worker when the file is first opened. - All of the URI <-> module name conversions now consistently go through `Server.documentUriFromModule?` and `moduleFromDocumentUri` to ensure that we don't have minor deviations for this conversion all over the place. - The threading of the source search path through the file worker (from `lake setup-file`) is removed. It turns out that `lake serve` already sets the correct source search path in the environment, so we can just always use the search path from the environment. - Since we can now answer more requests that need the .ileans in untitled files, a lot of the tests that test 'Go to definition' needed to be adjusted so that they use the information from the watchdog, not the file worker. As we load references asynchronously, this PR adds an internal `$/lean/waitForILeans` request that tests can use to wait for all .ilean files to be loaded and for the ilean references from the file worker for the current document version to be finalized. - As part of this PR, we noticed that the .ileans aren't available in the NixOS setup, so @Kha adjusted the Nix CI to fix this. ### Breaking changes - `Server.documentUriFromModule` has been renamed to `Server.documentUriFromModule?` and doesn't take a `SearchPath` argument anymore, as the `SearchPath` is now computed from the `LEAN_SRC_PATH` environment variable. It has also been moved from `Lean.Server.GoTo` to `Lean.Server.Utils`. - `Server.moduleFromDocumentUri` does not take a `SearchPath` argument anymore and won't return an `Option` anymore. It has also been moved from `Lean.Server.GoTo` to `Lean.Server.Utils`. - The `System.SearchPath.searchModuleNameOfUri` function has been removed. It is recommended to use `Server.moduleFromDocumentUri` instead. - The `initSrcSearchPath` function has been renamed to `getSrcSearchPath` and has been moved from `Lean.Util.Paths` to `Lean.Util.Path`. It also doesn't need to take a `pkgSearchPath` argument anymore. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
641 lines
36 KiB
Text
641 lines
36 KiB
Text
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 3, "character": 8}}
|
||
{"range":
|
||
{"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. \n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 7, "character": 8}}
|
||
{"range":
|
||
{"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. \n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 12, "character": 4}}
|
||
{"range":
|
||
{"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.zero : Nat\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 21, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 23}},
|
||
"contents": {"value": "My tactic ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 21, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 23}},
|
||
"contents": {"value": "My tactic ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 21, "character": 13}}
|
||
{"range":
|
||
{"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. \n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 28, "character": 6}}
|
||
{"range":
|
||
{"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\n***\n*import Init.Notation*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 28, "character": 32}}
|
||
{"range":
|
||
{"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. \n***\n*import Init.Notation*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 31, "character": 6}}
|
||
{"range":
|
||
{"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\n***\n*import Init.Notation*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 31, "character": 24}}
|
||
{"range":
|
||
{"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. \n***\n*import Init.Notation*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 36, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 23}},
|
||
"contents": {"value": "My tactic ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 44, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 23}},
|
||
"contents": {"value": "My tactic ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 49, "character": 16}}
|
||
{"range":
|
||
{"start": {"line": 49, "character": 15}, "end": {"line": 49, "character": 21}},
|
||
"contents":
|
||
{"value": "```lean\nmyNota : Lean.ParserDescr\n```\n***\nMy notation ",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 52, "character": 7}}
|
||
{"range":
|
||
{"start": {"line": 52, "character": 7}, "end": {"line": 52, "character": 15}},
|
||
"contents":
|
||
{"value": "```lean\n1 : Nat\n```\n***\nMy notation ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 59, "character": 7}}
|
||
{"range":
|
||
{"start": {"line": 59, "character": 7}, "end": {"line": 59, "character": 15}},
|
||
"contents":
|
||
{"value": "```lean\nNat\n```\n***\nMy notation ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 69, "character": 7}}
|
||
{"range":
|
||
{"start": {"line": 69, "character": 7}, "end": {"line": 69, "character": 16}},
|
||
"contents":
|
||
{"value": "```lean\nNat\n```\n***\nMy ultimate notation ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 73, "character": 21}}
|
||
{"range":
|
||
{"start": {"line": 73, "character": 18}, "end": {"line": 73, "character": 25}},
|
||
"contents":
|
||
{"value": "```lean\nmyInfix : Lean.TrailingParserDescr\n```",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 73, "character": 39}}
|
||
{"range":
|
||
{"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers, typically used via the `+` operator.\n\nThis function is overridden in both the kernel and the compiler to efficiently evaluate using the\narbitrary-precision arithmetic library. The definition provided here is the logical model.\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 77, "character": 10}}
|
||
{"range":
|
||
{"start": {"line": 77, "character": 7}, "end": {"line": 77, "character": 14}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat\n```\n***\nAddition of natural numbers, typically used via the `+` operator.\n\nThis function is overridden in both the kernel and the compiler to efficiently evaluate using the\narbitrary-precision arithmetic library. The definition provided here is the logical model.\n",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 82, "character": 7}}
|
||
{"range":
|
||
{"start": {"line": 82, "character": 7}, "end": {"line": 82, "character": 8}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat : Type\n```\n***\nThe natural numbers, starting at zero.\n\nThis type is special-cased by both the kernel and the compiler, and overridden with an efficient\nimplementation. Both use a fast arbitrary-precision arithmetic library (usually\n[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.\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```\n***\nA `doSeq` is a sequence of `doElem`, the main argument after the `do` keyword and other\ndo elements that take blocks. It can either have the form `\"{\" (doElem \";\"?)* \"}\"` or\n`many1Indent (doElem \";\"?)`, where `many1Indent` ensures that all the items are at\nthe same or higher indentation level as the first line. \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```\n***\nA `doSeq` is a sequence of `doElem`, the main argument after the `do` keyword and other\ndo elements that take blocks. It can either have the form `\"{\" (doElem \";\"?)* \"}\"` or\n`many1Indent (doElem \";\"?)`, where `many1Indent` ensures that all the items are at\nthe same or higher indentation level as the first line. \n***\n*import Lean.Parser.Do*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 92, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 92, "character": 0}, "end": {"line": 92, "character": 7}},
|
||
"contents": {"value": "My command ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 99, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 99, "character": 0}, "end": {"line": 99, "character": 7}},
|
||
"contents": {"value": "My command ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 102, "character": 16}}
|
||
{"range":
|
||
{"start": {"line": 102, "character": 16},
|
||
"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. \n***\n*import Lean.Parser.Extra*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 102, "character": 24}}
|
||
{"range":
|
||
{"start": {"line": 102, "character": 24},
|
||
"end": {"line": 102, "character": 31}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nLean.ParserDescr.sepBy1 (p : Lean.ParserDescr) (sep : String) (psep : Lean.ParserDescr)\n (allowTrailingSep : 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}}
|
||
{"range":
|
||
{"start": {"line": 102, "character": 31},
|
||
"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. \n***\n*import Init.Notation*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 111, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 111, "character": 0}, "end": {"line": 111, "character": 8}},
|
||
"contents": {"value": "My ultimate command ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 115, "character": 10}}
|
||
{"range":
|
||
{"start": {"line": 115, "character": 8},
|
||
"end": {"line": 115, "character": 14}},
|
||
"contents":
|
||
{"value":
|
||
"Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be\ninherited. If `e` is itself a variable called `x`, it can be elided:\n`fun y => { x := 1, y }`.\nA *structure update* of an existing value can be given via `with`:\n`{ point with x := 1 }`.\nThe structure type can be specified if not inferable:\n`{ x := 1, y := 2 : Point }`.\n",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 119, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 119, "character": 8},
|
||
"end": {"line": 119, "character": 10}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nid.{u} {α : Sort u} (a : α) : α\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}}
|
||
{"range":
|
||
{"start": {"line": 119, "character": 8},
|
||
"end": {"line": 119, "character": 21}},
|
||
"contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 126, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 126, "character": 2}, "end": {"line": 126, "character": 3}},
|
||
"contents": {"value": "```lean\nn : Id ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 133, "character": 9}}
|
||
{"range":
|
||
{"start": {"line": 133, "character": 7},
|
||
"end": {"line": 133, "character": 17}},
|
||
"contents": {"value": "```lean\nfoo : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 138, "character": 7}}
|
||
{"range":
|
||
{"start": {"line": 138, "character": 7},
|
||
"end": {"line": 138, "character": 10}},
|
||
"contents": {"value": "```lean\nBar.foo : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 141, "character": 9}}
|
||
{"range":
|
||
{"start": {"line": 141, "character": 7},
|
||
"end": {"line": 141, "character": 17}},
|
||
"contents": {"value": "```lean\n_root_.foo : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 144, "character": 4}}
|
||
{"range":
|
||
{"start": {"line": 144, "character": 4}, "end": {"line": 144, "character": 7}},
|
||
"contents": {"value": "```lean\nBar.bar : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 147, "character": 10}}
|
||
{"range":
|
||
{"start": {"line": 147, "character": 10},
|
||
"end": {"line": 147, "character": 13}},
|
||
"contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 147, "character": 17}}
|
||
{"range":
|
||
{"start": {"line": 147, "character": 17},
|
||
"end": {"line": 147, "character": 19}},
|
||
"contents":
|
||
{"value": "```lean\nBar.Foo.mk (hi : ℕ) : Foo\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 150, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 150, "character": 2}, "end": {"line": 150, "character": 4}},
|
||
"contents":
|
||
{"value": "```lean\nBar.Foo.hi (self : Foo) : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 153, "character": 10}}
|
||
{"range":
|
||
{"start": {"line": 153, "character": 10},
|
||
"end": {"line": 153, "character": 13}},
|
||
"contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 155, "character": 4}}
|
||
{"range":
|
||
{"start": {"line": 155, "character": 4}, "end": {"line": 155, "character": 6}},
|
||
"contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 158, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 158, "character": 0}, "end": {"line": 158, "character": 8}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nBar.«instToStringNat_external:file:///hover.lean» : ToString ℕ\n```",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 160, "character": 9}}
|
||
{"range":
|
||
{"start": {"line": 160, "character": 9},
|
||
"end": {"line": 160, "character": 10}},
|
||
"contents": {"value": "```lean\nBar.f : ToString ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 163, "character": 10}}
|
||
{"range":
|
||
{"start": {"line": 163, "character": 10},
|
||
"end": {"line": 163, "character": 16}},
|
||
"contents":
|
||
{"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 166, "character": 4}}
|
||
{"range":
|
||
{"start": {"line": 166, "character": 4},
|
||
"end": {"line": 166, "character": 11}},
|
||
"contents": {"value": "```lean\nBar.foo.bar : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 166, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 166, "character": 4},
|
||
"end": {"line": 166, "character": 11}},
|
||
"contents": {"value": "```lean\nBar.foo.bar : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 173, "character": 6}}
|
||
{"range":
|
||
{"start": {"line": 173, "character": 6}, "end": {"line": 173, "character": 7}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 176, "character": 4}}
|
||
[{"uri": "file:///hover.lean",
|
||
"range":
|
||
{"start": {"line": 173, "character": 6},
|
||
"end": {"line": 173, "character": 7}}}]
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 176, "character": 4}}
|
||
{"range":
|
||
{"start": {"line": 176, "character": 4}, "end": {"line": 176, "character": 5}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 180, "character": 12}}
|
||
{"range":
|
||
{"start": {"line": 180, "character": 11},
|
||
"end": {"line": 180, "character": 33}},
|
||
"contents":
|
||
{"value": "Enables or disables all unused variable linter warnings ",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 183, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 183, "character": 8}, "end": {"line": 183, "character": 9}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 186, "character": 8}}
|
||
[{"uri": "file:///hover.lean",
|
||
"range":
|
||
{"start": {"line": 183, "character": 8},
|
||
"end": {"line": 183, "character": 9}}}]
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 186, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 186, "character": 8}, "end": {"line": 186, "character": 9}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 191, "character": 25}}
|
||
{"range":
|
||
{"start": {"line": 191, "character": 25},
|
||
"end": {"line": 191, "character": 26}},
|
||
"contents": {"value": "```lean\nn : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 194, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 194, "character": 0}, "end": {"line": 194, "character": 9}},
|
||
"contents":
|
||
{"value":
|
||
"`declModifiers` is the collection of modifiers on a declaration:\n* a doc comment `/-- ... -/`\n* a list of attributes `@[attr1, attr2]`\n* a visibility specifier, `private` or `protected`\n* `noncomputable`\n* `unsafe`\n* `partial` or `nonrec`\n\nAll modifiers are optional, and have to come in the listed order.\n\n`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed\non the same line as the declaration. It is used for declarations nested inside other syntax,\nsuch as inductive constructors, structure projections, and `let rec` / `where` definitions. ",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 200, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 200, "character": 2},
|
||
"end": {"line": 200, "character": 15}},
|
||
"contents":
|
||
{"value":
|
||
"`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 203, "character": 28}}
|
||
{"range":
|
||
{"start": {"line": 203, "character": 27},
|
||
"end": {"line": 203, "character": 32}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nId ℕ\n```\n***\nParentheses, used for grouping expressions (e.g., `a * (b + c)`).\nCan also be used for creating simple functions when combined with `·`. Here are some examples:\n - `(· + 1)` is shorthand for `fun x => x + 1`\n - `(· + ·)` is shorthand for `fun x y => x + y`\n - `(f · a b)` is shorthand for `fun x => f x a b`\n - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n - also applies to other parentheses-like notations such as `(·, 1)`\n",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 206, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 206, "character": 8}, "end": {"line": 206, "character": 9}},
|
||
"contents": {"value": "```lean\n?m\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 206, "character": 10}}
|
||
{"range":
|
||
{"start": {"line": 206, "character": 8},
|
||
"end": {"line": 206, "character": 13}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\n?m x1✝ x2✝\n```\n***\n`a + b` computes the sum of `a` and `b`.\nThe meaning of this notation is type-dependent. \n\nConventions for notations in identifiers:\n\n * The recommended spelling of `+` in identifiers is `add`.",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 215, "character": 28}}
|
||
{"range":
|
||
{"start": {"line": 215, "character": 28},
|
||
"end": {"line": 215, "character": 29}},
|
||
"contents": {"value": "```lean\nx : α\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 217, "character": 28}}
|
||
{"range":
|
||
{"start": {"line": 217, "character": 28},
|
||
"end": {"line": 217, "character": 29}},
|
||
"contents": {"value": "```lean\nα\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 219, "character": 31}}
|
||
{"range":
|
||
{"start": {"line": 219, "character": 31},
|
||
"end": {"line": 219, "character": 32}},
|
||
"contents": {"value": "```lean\nx : α\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 222, "character": 22}}
|
||
{"range":
|
||
{"start": {"line": 222, "character": 22},
|
||
"end": {"line": 222, "character": 32}},
|
||
"contents": {"value": "my_intro tactic ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 222, "character": 31}}
|
||
{"range":
|
||
{"start": {"line": 222, "character": 31},
|
||
"end": {"line": 222, "character": 32}},
|
||
"contents": {"value": "```lean\nα\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 229, "character": 22}}
|
||
{"range":
|
||
{"start": {"line": 229, "character": 22},
|
||
"end": {"line": 229, "character": 32}},
|
||
"contents": {"value": "my_intro tactic ", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 231, "character": 17}}
|
||
{"range":
|
||
{"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": 238, "character": 4}}
|
||
{"range":
|
||
{"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": 241, "character": 4}}
|
||
{"range":
|
||
{"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": 241, "character": 9}}
|
||
{"range":
|
||
{"start": {"line": 241, "character": 9},
|
||
"end": {"line": 241, "character": 10}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 245, "character": 8}}
|
||
{"range":
|
||
{"start": {"line": 245, "character": 8}, "end": {"line": 245, "character": 9}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 247, "character": 12}}
|
||
{"range":
|
||
{"start": {"line": 247, "character": 12},
|
||
"end": {"line": 247, "character": 13}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 249, "character": 4}}
|
||
{"range":
|
||
{"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": 252, "character": 9}}
|
||
{"range":
|
||
{"start": {"line": 252, "character": 9},
|
||
"end": {"line": 252, "character": 10}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 252, "character": 11}}
|
||
{"range":
|
||
{"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": 257, "character": 6}}
|
||
{"range":
|
||
{"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 257, "character": 15}}
|
||
{"range":
|
||
{"start": {"line": 257, "character": 13},
|
||
"end": {"line": 257, "character": 18}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 260, "character": 6}}
|
||
{"range":
|
||
{"start": {"line": 260, "character": 4}, "end": {"line": 260, "character": 9}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 260, "character": 17}}
|
||
{"range":
|
||
{"start": {"line": 260, "character": 15},
|
||
"end": {"line": 260, "character": 20}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 263, "character": 27}}
|
||
{"range":
|
||
{"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": 263, "character": 28}}
|
||
{"range":
|
||
{"start": {"line": 263, "character": 28},
|
||
"end": {"line": 263, "character": 36}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 269, "character": 2}}
|
||
{"range":
|
||
{"start": {"line": 269, "character": 2}, "end": {"line": 269, "character": 3}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 272, "character": 4}}
|
||
{"range":
|
||
{"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": 277, "character": 22}}
|
||
{"range":
|
||
{"start": {"line": 277, "character": 22},
|
||
"end": {"line": 277, "character": 23}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 277, "character": 13}}
|
||
{"range":
|
||
{"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": 282, "character": 8}}
|
||
{"range":
|
||
{"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": 285, "character": 9}}
|
||
{"range":
|
||
{"start": {"line": 285, "character": 9},
|
||
"end": {"line": 285, "character": 10}},
|
||
"contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 290, "character": 13}}
|
||
{"range":
|
||
{"start": {"line": 290, "character": 13},
|
||
"end": {"line": 290, "character": 16}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nList.nil.{u} {α : Type u} : List α\n```\n***\nThe empty list, usually written `[]`. \n\nConventions for notations in identifiers:\n\n * The recommended spelling of `[]` in identifiers is `nil`.\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 292, "character": 13}}
|
||
{"range":
|
||
{"start": {"line": 292, "character": 11},
|
||
"end": {"line": 292, "character": 15}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nList.cons.{u} {α : Type u} (head : α) (tail : List α) : List α\n```\n***\nThe list whose first element is `head`, where `tail` is the rest of the list.\nUsually written `head :: tail`.\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `::` in identifiers is `cons`.\n\n * The recommended spelling of `[a]` in identifiers is `singleton`.\n***\n*import Init.Prelude*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 294, "character": 18}}
|
||
{"range":
|
||
{"start": {"line": 294, "character": 17},
|
||
"end": {"line": 294, "character": 20}},
|
||
"contents":
|
||
{"value":
|
||
"```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (l : List α) : List β\n```\n***\nApplies a function to each element of the list, returning the resulting list of values.\n\n`O(|l|)`.\n\nExamples:\n* `[a, b, c].map f = [f a, f b, f c]`\n* `[].map Nat.succ = []`\n* `[\"one\", \"two\", \"three\"].map (·.length) = [3, 3, 5]`\n* `[\"one\", \"two\", \"three\"].map (·.reverse) = [\"eno\", \"owt\", \"eerht\"]`\n\n***\n*import Init.Data.List.Basic*",
|
||
"kind": "markdown"}}
|
||
{"textDocument": {"uri": "file:///hover.lean"},
|
||
"position": {"line": 297, "character": 26}}
|
||
{"range":
|
||
{"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***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [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": 297, "character": 19}}
|
||
{"range":
|
||
{"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***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
|
||
"kind": "markdown"}}
|