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

feat: add declId hover for syntax/notation/mixfix

Browse source
This commit is contained in:
Mario Carneiro 2022-08-14 19:05:54 -04:00 • committed by Leonardo de Moura
parent fd11e662b0
commit 37a12b635b
9 changed files with 139 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/ElabRules.lean
View file

@ -88,7 +88,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
@[builtinCommandElab Lean.Parser.Command.elab]
def elabElab : CommandElab
| `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
elab$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* :
elab%$tk$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* :
$cat $[<= $expectedType?]? => $rhs) => do
let prio ← liftMacroM <| evalOptPrio prio?
let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
@ -96,9 +96,12 @@ def elabElab : CommandElab
let name ← match name? with
| some name => pure name.getId
| none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
let nameId := name?.getD (mkIdentFrom tk name)
let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
`($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio):num) $[$stxParts]* : $cat
$[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) >>= (elabCommand ·)
elabCommand <|← `(
$[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
syntax%$tk$[:$prec?]? (name := $nameId) (priority := $(quote prio):num) $[$stxParts]* : $cat
$[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs)
| _ => throwUnsupportedSyntax
end Lean.Elab.Command

4
src/Lean/Elab/InfoTree/Main.lean
View file

@ -290,8 +290,8 @@ def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MV
let info ← mkInfo a
modifyInfoTrees fun trees =>
match info with
| Sum.inl info => treesSaved.push <| InfoTree.node info trees
| Sum.inr mvaId => treesSaved.push <| InfoTree.hole mvaId
| Sum.inl info => treesSaved.push <| InfoTree.node info trees
| Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
else
x

2
src/Lean/Elab/Macro.lean
View file

@ -25,7 +25,7 @@ open Lean.Parser.Command
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
let stxCmd ← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio):num) $[$stxParts]* : $cat)
syntax$[:$prec?]? (name := $(name?.getD (mkIdentFrom tk name))) (priority := $(quote prio):num) $[$stxParts]* : $cat)
let rhs := rhs.raw
let macroRulesCmd ← if rhs.getArgs.size == 1 then
-- `rhs` is a `term`

2
src/Lean/Elab/Notation.lean
View file

@ -143,7 +143,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
let fullName := currNamespace ++ name
let pat : Term := ⟨mkNode fullName patArgs⟩
let stxDecl ← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio)) $[$syntaxParts]* : $cat)
syntax $[: $prec?]? (name := $(name?.getD (mkIdent name))) (priority := $(quote prio)) $[$syntaxParts]* : $cat)
let macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
let macroDecls ←
if isLocalAttrKind attrKind then

8
src/Lean/Elab/Syntax.lean
View file

@ -341,7 +341,8 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
throwError "invalid syntax node kind '{k}'"
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind syntax $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) ← pure stx
let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind
syntax%$tk $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) := stx
| throwUnsupportedSyntax
let cat := catStx.getId.eraseMacroScopes
unless (Parser.isParserCategory (← getEnv) cat) do
@ -357,10 +358,11 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
| some name => pure name.getId
| none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
let prio ← liftMacroM <| evalOptPrio prio?
let idRef := (name?.map (·.raw)).getD tk
let stxNodeKind := (← getCurrNamespace) ++ name
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser")
let catParserId := mkIdentFrom idRef (cat.appendAfter "Parser")
let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser cat
let declName := mkIdentFrom stx name
let declName := name?.getD (mkIdentFrom idRef name)
let attrInstance ← `(attrInstance| $attrKind:attrKind $catParserId:ident $(quote prio):num)
let attrInstances := attrInstances.getD { elemsAndSeps := #[] }
let attrInstances := attrInstances.push attrInstance

2
src/Lean/Elab/Term.lean
View file

@ -346,7 +346,7 @@ def withoutModifyingElabMetaStateWithInfo (x : TermElabM α) : TermElabM α := d
set sMeta
/--
Execute `x` bud discard changes performed to the state.
Execute `x` but discard changes performed to the state.
However, the info trees and messages are not discarded. -/
private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : TermElabM α := do
let saved ← saveState

3
tests/lean/interactive/goTo.lean.expected.out
View file

@ -78,7 +78,8 @@
"position": {"line": 43, "character": 7}}
[{"targetUri": "file://goTo.lean",
"targetSelectionRange":
{"start": {"line": 36, "character": 0}, "end": {"line": 36, "character": 39}},
{"start": {"line": 36, "character": 16},
"end": {"line": 36, "character": 24}},
"targetRange":
{"start": {"line": 36, "character": 0}, "end": {"line": 36, "character": 39}},
"originSelectionRange":

3
tests/lean/interactive/hover.lean
View file

@ -47,7 +47,8 @@ example : True := by
/-- My notation -/
macro "mynota" e:term : term => pure e
macro (name := myNota) "mynota" e:term : term => pure e
--^ textDocument/hover
#check mynota 1
--^ textDocument/hover

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

@ -83,272 +83,283 @@
{"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 23}},
"contents": {"value": "My tactic ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 51, "character": 7}}
"position": {"line": 49, "character": 16}}
{"range":
{"start": {"line": 51, "character": 7}, "end": {"line": 51, "character": 15}},
{"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": 58, "character": 7}}
"position": {"line": 59, "character": 7}}
{"range":
{"start": {"line": 58, "character": 7}, "end": {"line": 58, "character": 15}},
{"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": 68, "character": 7}}
"position": {"line": 69, "character": 7}}
{"range":
{"start": {"line": 68, "character": 7}, "end": {"line": 68, "character": 16}},
{"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": 72, "character": 21}}
null
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 72, "character": 39}}
"position": {"line": 73, "character": 21}}
{"range":
{"start": {"line": 72, "character": 38}, "end": {"line": 72, "character": 45}},
{"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.\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",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 76, "character": 10}}
"position": {"line": 77, "character": 10}}
{"range":
{"start": {"line": 76, "character": 7}, "end": {"line": 76, "character": 14}},
{"start": {"line": 77, "character": 7}, "end": {"line": 77, "character": 14}},
"contents":
{"value":
"```lean\nNat\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",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 81, "character": 14}}
"position": {"line": 82, "character": 14}}
{"range":
{"start": {"line": 81, "character": 14}, "end": {"line": 81, "character": 36}},
{"start": {"line": 82, "character": 14}, "end": {"line": 82, "character": 36}},
"contents":
{"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 83, "character": 30}}
"position": {"line": 84, "character": 30}}
{"range":
{"start": {"line": 83, "character": 29}, "end": {"line": 83, "character": 34}},
{"start": {"line": 84, "character": 29}, "end": {"line": 84, "character": 34}},
"contents":
{"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 86, "character": 2}}
"position": {"line": 87, "character": 2}}
{"range":
{"start": {"line": 86, "character": 0}, "end": {"line": 86, "character": 7}},
{"start": {"line": 87, "character": 0}, "end": {"line": 87, "character": 7}},
"contents": {"value": "My command ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 93, "character": 2}}
"position": {"line": 94, "character": 2}}
{"range":
{"start": {"line": 93, "character": 0}, "end": {"line": 93, "character": 7}},
{"start": {"line": 94, "character": 0}, "end": {"line": 94, "character": 7}},
"contents": {"value": "My command ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 96, "character": 16}}
"position": {"line": 97, "character": 16}}
{"range":
{"start": {"line": 96, "character": 16}, "end": {"line": 96, "character": 23}},
{"start": {"line": 97, "character": 16}, "end": {"line": 97, "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. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 96, "character": 24}}
"position": {"line": 97, "character": 24}}
{"range":
{"start": {"line": 96, "character": 24}, "end": {"line": 96, "character": 31}},
{"start": {"line": 97, "character": 24}, "end": {"line": 97, "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`. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 96, "character": 31}}
"position": {"line": 97, "character": 31}}
{"range":
{"start": {"line": 96, "character": 31}, "end": {"line": 96, "character": 35}},
{"start": {"line": 97, "character": 31}, "end": {"line": 97, "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. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 105, "character": 2}}
"position": {"line": 106, "character": 2}}
{"range":
{"start": {"line": 105, "character": 0}, "end": {"line": 105, "character": 8}},
{"start": {"line": 106, "character": 0}, "end": {"line": 106, "character": 8}},
"contents": {"value": "My ultimate command ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 109, "character": 10}}
"position": {"line": 110, "character": 10}}
null
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 113, "character": 8}}
"position": {"line": 114, "character": 8}}
{"range":
{"start": {"line": 113, "character": 8},
"end": {"line": 113, "character": 10}},
{"start": {"line": 114, "character": 8},
"end": {"line": 114, "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",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 113, "character": 10}}
"position": {"line": 114, "character": 10}}
{"range":
{"start": {"line": 113, "character": 8},
"end": {"line": 113, "character": 21}},
{"start": {"line": 114, "character": 8},
"end": {"line": 114, "character": 21}},
"contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 120, "character": 2}}
"position": {"line": 121, "character": 2}}
{"range":
{"start": {"line": 120, "character": 2}, "end": {"line": 120, "character": 3}},
{"start": {"line": 121, "character": 2}, "end": {"line": 121, "character": 3}},
"contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 127, "character": 9}}
"position": {"line": 128, "character": 9}}
{"range":
{"start": {"line": 127, "character": 7},
"end": {"line": 127, "character": 17}},
{"start": {"line": 128, "character": 7},
"end": {"line": 128, "character": 17}},
"contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 132, "character": 7}}
"position": {"line": 133, "character": 7}}
{"range":
{"start": {"line": 132, "character": 7},
"end": {"line": 132, "character": 10}},
{"start": {"line": 133, "character": 7},
"end": {"line": 133, "character": 10}},
"contents": {"value": "```lean\nBar.foo : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 135, "character": 9}}
"position": {"line": 136, "character": 9}}
{"range":
{"start": {"line": 135, "character": 7},
"end": {"line": 135, "character": 17}},
{"start": {"line": 136, "character": 7},
"end": {"line": 136, "character": 17}},
"contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 138, "character": 4}}
"position": {"line": 139, "character": 4}}
{"range":
{"start": {"line": 138, "character": 4}, "end": {"line": 138, "character": 7}},
{"start": {"line": 139, "character": 4}, "end": {"line": 139, "character": 7}},
"contents": {"value": "```lean\nBar.bar : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 141, "character": 10}}
"position": {"line": 142, "character": 10}}
{"range":
{"start": {"line": 141, "character": 10},
"end": {"line": 141, "character": 13}},
{"start": {"line": 142, "character": 10},
"end": {"line": 142, "character": 13}},
"contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 141, "character": 17}}
"position": {"line": 142, "character": 17}}
{"range":
{"start": {"line": 141, "character": 17},
"end": {"line": 141, "character": 19}},
{"start": {"line": 142, "character": 17},
"end": {"line": 142, "character": 19}},
"contents":
{"value": "```lean\nBar.Foo.mk : Nat → Foo\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 144, "character": 2}}
"position": {"line": 145, "character": 2}}
{"range":
{"start": {"line": 144, "character": 2}, "end": {"line": 144, "character": 4}},
{"start": {"line": 145, "character": 2}, "end": {"line": 145, "character": 4}},
"contents":
{"value": "```lean\nBar.Foo.hi : Foo → Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 147, "character": 10}}
"position": {"line": 148, "character": 10}}
{"range":
{"start": {"line": 147, "character": 10},
"end": {"line": 147, "character": 13}},
{"start": {"line": 148, "character": 10},
"end": {"line": 148, "character": 13}},
"contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 149, "character": 4}}
"position": {"line": 150, "character": 4}}
{"range":
{"start": {"line": 149, "character": 4}, "end": {"line": 149, "character": 6}},
{"start": {"line": 150, "character": 4}, "end": {"line": 150, "character": 6}},
"contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 152, "character": 2}}
"position": {"line": 153, "character": 2}}
{"range":
{"start": {"line": 152, "character": 0}, "end": {"line": 152, "character": 8}},
{"start": {"line": 153, "character": 0}, "end": {"line": 153, "character": 8}},
"contents":
{"value": "```lean\nBar.instToStringNat : ToString Nat\n```",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 154, "character": 9}}
"position": {"line": 155, "character": 9}}
{"range":
{"start": {"line": 154, "character": 9},
"end": {"line": 154, "character": 10}},
{"start": {"line": 155, "character": 9},
"end": {"line": 155, "character": 10}},
"contents":
{"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 157, "character": 10}}
"position": {"line": 158, "character": 10}}
{"range":
{"start": {"line": 157, "character": 10},
"end": {"line": 157, "character": 16}},
{"start": {"line": 158, "character": 10},
"end": {"line": 158, "character": 16}},
"contents":
{"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 160, "character": 4}}
"position": {"line": 161, "character": 4}}
{"range":
{"start": {"line": 160, "character": 4},
"end": {"line": 160, "character": 11}},
{"start": {"line": 161, "character": 4},
"end": {"line": 161, "character": 11}},
"contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 160, "character": 8}}
"position": {"line": 161, "character": 8}}
{"range":
{"start": {"line": 160, "character": 4},
"end": {"line": 160, "character": 11}},
{"start": {"line": 161, "character": 4},
"end": {"line": 161, "character": 11}},
"contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 165, "character": 6}}
"position": {"line": 166, "character": 6}}
{"range":
{"start": {"line": 165, "character": 6}, "end": {"line": 165, "character": 7}},
{"start": {"line": 166, "character": 6}, "end": {"line": 166, "character": 7}},
"contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 168, "character": 4}}
"position": {"line": 169, "character": 4}}
[{"targetUri": "file://hover.lean",
"targetSelectionRange":
{"start": {"line": 165, "character": 6},
"end": {"line": 165, "character": 7}},
{"start": {"line": 166, "character": 6},
"end": {"line": 166, "character": 7}},
"targetRange":
{"start": {"line": 165, "character": 6},
"end": {"line": 165, "character": 7}},
{"start": {"line": 166, "character": 6},
"end": {"line": 166, "character": 7}},
"originSelectionRange":
{"start": {"line": 168, "character": 4},
"end": {"line": 168, "character": 5}}}]
{"start": {"line": 169, "character": 4},
"end": {"line": 169, "character": 5}}}]
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 168, "character": 4}}
"position": {"line": 169, "character": 4}}
{"range":
{"start": {"line": 168, "character": 4}, "end": {"line": 168, "character": 5}},
{"start": {"line": 169, "character": 4}, "end": {"line": 169, "character": 5}},
"contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 172, "character": 8}}
"position": {"line": 173, "character": 8}}
{"range":
{"start": {"line": 172, "character": 8}, "end": {"line": 172, "character": 9}},
{"start": {"line": 173, "character": 8}, "end": {"line": 173, "character": 9}},
"contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 175, "character": 8}}
"position": {"line": 176, "character": 8}}
[{"targetUri": "file://hover.lean",
"targetSelectionRange":
{"start": {"line": 172, "character": 8},
"end": {"line": 172, "character": 9}},
{"start": {"line": 173, "character": 8},
"end": {"line": 173, "character": 9}},
"targetRange":
{"start": {"line": 172, "character": 8},
"end": {"line": 172, "character": 9}},
{"start": {"line": 173, "character": 8},
"end": {"line": 173, "character": 9}},
"originSelectionRange":
{"start": {"line": 175, "character": 8},
"end": {"line": 175, "character": 9}}}]
{"start": {"line": 176, "character": 8},
"end": {"line": 176, "character": 9}}}]
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 175, "character": 8}}
"position": {"line": 176, "character": 8}}
{"range":
{"start": {"line": 175, "character": 8}, "end": {"line": 175, "character": 9}},
{"start": {"line": 176, "character": 8}, "end": {"line": 176, "character": 9}},
"contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 180, "character": 25}}
"position": {"line": 181, "character": 25}}
{"range":
{"start": {"line": 180, "character": 25},
"end": {"line": 180, "character": 26}},
{"start": {"line": 181, "character": 25},
"end": {"line": 181, "character": 26}},
"contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 183, "character": 2}}
"position": {"line": 184, "character": 2}}
null
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 189, "character": 2}}
"position": {"line": 190, "character": 2}}
{"range":
{"start": {"line": 189, "character": 2},
"end": {"line": 189, "character": 15}},
{"start": {"line": 190, "character": 2},
"end": {"line": 190, "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": 192, "character": 28}}
"position": {"line": 193, "character": 28}}
{"range":
{"start": {"line": 192, "character": 27},
"end": {"line": 192, "character": 32}},
{"start": {"line": 193, "character": 27},
"end": {"line": 193, "character": 32}},
"contents":
{"value":
"```lean\nId Nat\n```\n***\nYou can use parentheses for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- 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",