From 37a12b635b61eba70ff2be9a29422ef3daaa6fc9 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 14 Aug 2022 19:05:54 -0400 Subject: [PATCH] feat: add declId hover for syntax/notation/mixfix --- src/Lean/Elab/ElabRules.lean | 9 +- src/Lean/Elab/InfoTree/Main.lean | 4 +- src/Lean/Elab/Macro.lean | 2 +- src/Lean/Elab/Notation.lean | 2 +- src/Lean/Elab/Syntax.lean | 8 +- src/Lean/Elab/Term.lean | 2 +- tests/lean/interactive/goTo.lean.expected.out | 3 +- tests/lean/interactive/hover.lean | 3 +- .../lean/interactive/hover.lean.expected.out | 227 +++++++++--------- 9 files changed, 139 insertions(+), 121 deletions(-) diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index 2183477780..1a6d6826d0 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -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 diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 35f465a722..c9b9a9f98b 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -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 diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean index cc72665f1e..00108fba88 100644 --- a/src/Lean/Elab/Macro.lean +++ b/src/Lean/Elab/Macro.lean @@ -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` diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean index 93c58e63ae..6680bc5a15 100644 --- a/src/Lean/Elab/Notation.lean +++ b/src/Lean/Elab/Notation.lean @@ -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 diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index caa5c1f925..eb42dedbd7 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 1c2042c9fb..d9bc527a75 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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 diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out index 94c896fb1e..3b2e845d3e 100644 --- a/tests/lean/interactive/goTo.lean.expected.out +++ b/tests/lean/interactive/goTo.lean.expected.out @@ -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": diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index 7d6bd283b9..3fd024384e 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -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 diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 58bc386d73..d76a9952fc 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -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",