From 9fbbe6554d8aab46cd42a98353b664b63b019b92 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 20 Jan 2026 12:12:05 +0100 Subject: [PATCH] fix: make first token detection work in modules (#12047) This PR makes the automatic first token detection in tactic docs much more robust, in addition to making it work in modules and other contexts where builtin tactics are not in the environment. It also adds the ability to override the tactic's first token as the user-visible name. Previously, first token detection would look up the parser descriptor in the environment and process its syntax. This would be incorrect for builtin parsers, as well as for modules in which the definition is not loaded. Now, it instead consults the Pratt parsing table for the `tactic` syntax category. Tests are added that ensure this keeps working in modules, and also that the first token of all tactics that ship with Lean are either detected unambiguously or annotated to remove ambiguity. Closes #12038. --- src/Init/Tactics.lean | 60 +- src/Lean/Elab/Tactic/Doc.lean | 103 +- src/Lean/Parser/Attr.lean | 17 +- src/Lean/Parser/Tactic.lean | 19 +- src/Lean/Parser/Tactic/Doc.lean | 78 +- .../Completion/CompletionCollectors.lean | 3 +- src/Std/Tactic/Do/Syntax.lean | 1 + stage0/src/stdlib_flags.h | 1 + tests/lean/interactive/completionTactics.lean | 14 + .../completionTactics.lean.expected.out | 905 +++++++----------- tests/lean/run/tacticDoc.lean | 67 +- tests/lean/run/tacticDocAllModule.lean | 25 + tests/lean/run/tacticDocAllNonmod.lean | 23 + tests/lean/run/tacticDocUserName.lean | 61 ++ 14 files changed, 739 insertions(+), 638 deletions(-) create mode 100644 tests/lean/run/tacticDocAllModule.lean create mode 100644 tests/lean/run/tacticDocAllNonmod.lean create mode 100644 tests/lean/run/tacticDocUserName.lean diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 6b67701de9..2834a21553 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -518,14 +518,13 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp) assuming these are definitionally equal. * `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming assuming `t` and `t'` are definitionally equal. --/ -syntax (name := change) "change " term (location)? : tactic - -/-- * `change a with b` will change occurrences of `a` to `b` in the goal, assuming `a` and `b` are definitionally equal. * `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`. -/ +syntax (name := change) "change " term (location)? : tactic + +@[tactic_alt change] syntax (name := changeWith) "change " term " with " term (location)? : tactic /-- @@ -905,8 +904,13 @@ The tactic supports all the same syntax variants and options as the `let` term. -/ macro "let" c:letConfig d:letDecl : tactic => `(tactic| refine_lift let $c:letConfig $d:letDecl; ?_) -/-- `let rec f : t := e` adds a recursive definition `f` to the current goal. -The syntax is the same as term-mode `let rec`. -/ +/-- +`let rec f : t := e` adds a recursive definition `f` to the current goal. +The syntax is the same as term-mode `let rec`. + +The tactic supports all the same syntax variants and options as the `let` term. +-/ +-- Uncomment after stage0 update: @[tactic_name "let rec"] syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic macro_rules | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_) @@ -1212,22 +1216,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`. syntax (name := congr) "congr" (ppSpace num)? : tactic -/-- -In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for: -``` -by_cases h : t -· tac1 -· tac2 -``` -It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs. - -You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but -if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed -by the end of the block. --/ -syntax (name := tacDepIfThenElse) - ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq) - ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic /-- In tactic mode, `if t then tac1 else tac2` is alternative syntax for: @@ -1236,16 +1224,34 @@ by_cases t · tac1 · tac2 ``` -It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous -hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use -nondependent `if`, since this wouldn't add anything to the context and hence would be -useless for proving theorems. To actually insert an `ite` application use -`refine if t then ?_ else ?_`.) +It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and +`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't +add anything to the context and hence would be useless for proving theorems. To actually insert an +`ite` application use `refine if t then ?_ else ?_`.) + +The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as +alternative syntax for: +``` +by_cases h : t +· tac1 +· tac2 +``` +It performs case distinction on `h : t` or `h : ¬t`. + +You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but +if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed +by the end of the block. -/ syntax (name := tacIfThenElse) ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq) ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic + +@[tactic_alt tacIfThenElse] +syntax (name := tacDepIfThenElse) + ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq) + ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic + /-- The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an empty pattern match, closing the goal if the introduced pattern is impossible. diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean index 426b857437..db0575d024 100644 --- a/src/Lean/Elab/Tactic/Doc.lean +++ b/src/Lean/Elab/Tactic/Doc.lean @@ -8,6 +8,7 @@ module prelude import Lean.DocString public import Lean.Elab.Command +public import Lean.Parser.Tactic.Doc public section @@ -38,30 +39,42 @@ open Lean.Parser.Command | _ => throwError "Malformed 'register_tactic_tag' command" /-- -Gets the first string token in a parser description. For example, for a declaration like -`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration -like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`. - -Returns `none` for syntax declarations that don't contain a string constant. +Computes a table that heuristically maps parser syntax kinds to their first tokens by inspecting the +Pratt parsing tables for the `tactic syntax kind. If a custom name is provided for the tactic, then +it is returned instead. -/ -private partial def getFirstTk (e : Expr) : MetaM (Option String) := do - match (← Meta.whnf e).getAppFnArgs with - | (``ParserDescr.node, #[_, _, p]) => getFirstTk p - | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p - | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p - | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p - | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p - | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk) - | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk) - | (``Parser.withAntiquot, #[_, p]) => getFirstTk p - | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p - | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) => - if let some tk ← getFirstTk p1 then pure (some tk) - else getFirstTk (.app p2 (.const ``Unit.unit [])) - | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk) - | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk) - | _ => pure none +def firstTacticTokens [Monad m] [MonadEnv m] : m (NameMap String) := do + let env ← getEnv + let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic + | return {} + + let mut firstTokens : NameMap String := + tacticNameExt.toEnvExtension.getState env + |>.importedEntries + |>.push (tacticNameExt.exportEntriesFn env (tacticNameExt.getState env) .exported) + |>.foldl (init := {}) fun names inMods => + inMods.foldl (init := names) fun names (k, n) => + names.insert k n + + firstTokens := addFirstTokens tactics tactics.tables.leadingTable firstTokens + firstTokens := addFirstTokens tactics tactics.tables.trailingTable firstTokens + + return firstTokens +where + addFirstTokens tactics table firsts : NameMap String := Id.run do + let mut firsts := firsts + for (tok, ps) in table do + -- Skip antiquotes + if tok == `«$» then continue + for (p, _) in ps do + for (k, ()) in p.info.collectKinds {} do + if tactics.kinds.contains k then + let tok := tok.toString (escape := false) + -- It's important here that the already-existing mapping is preserved, because it will + -- contain any user-provided custom name, and these shouldn't be overridden. + firsts := firsts.alter k (·.getD tok) + return firsts /-- Creates some `MessageData` for a parser name. @@ -71,18 +84,14 @@ identifiable leading token, then that token is shown. Otherwise, the underlying without an `@`. The name includes metadata that makes infoview hovers and the like work. This only works for global constants, as the local context is not included. -/ -private def showParserName (n : Name) : MetaM MessageData := do +private def showParserName [Monad m] [MonadEnv m] (firsts : NameMap String) (n : Name) : m MessageData := do let env ← getEnv let params := env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD [] - let tok ← - if let some descr := env.find? n |>.bind (·.value?) then - if let some tk ← getFirstTk descr then - pure <| Std.Format.text tk.trimAscii.copy - else pure <| format n - else pure <| format n + + let tok := ((← customTacticName n) <|> firsts.get? n).map Std.Format.text |>.getD (format n) pure <| .ofFormatWithInfos { - fmt := "'" ++ .tag 0 tok ++ "'", + fmt := "`" ++ .tag 0 tok ++ "`", infos := .ofList [(0, .ofTermInfo { lctx := .empty, @@ -93,7 +102,6 @@ private def showParserName (n : Name) : MetaM MessageData := do })] _ } - /-- Displays all available tactic tags, with documentation. -/ @@ -106,20 +114,22 @@ Displays all available tactic tags, with documentation. for (tac, tag) in arr do mapping := mapping.insert tag (mapping.getD tag {} |>.insert tac) + let firsts ← firstTacticTokens + let showDocs : Option String → MessageData | none => .nil | some d => Format.line ++ MessageData.joinSep ((d.split '\n').map (toMessageData ∘ String.Slice.copy)).toList Format.line - let showTactics (tag : Name) : MetaM MessageData := do + let showTactics (tag : Name) : CommandElabM MessageData := do match mapping.find? tag with | none => pure .nil | some tacs => if tacs.isEmpty then pure .nil else let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList - pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ") + pure (Format.line ++ MessageData.joinSep (← tacs.mapM (showParserName firsts)) ", ") - let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do + let tagDescrs ← (← allTagsWithInfo).mapM fun (name, userName, docs) => do pure <| m!"• " ++ MessageData.nestD (m!"`{name}`" ++ (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++ @@ -146,13 +156,13 @@ structure TacticDoc where /-- Any docstring extensions that have been specified -/ extensionDocs : Array String -def allTacticDocs : MetaM (Array TacticDoc) := do +def allTacticDocs (includeUnnamed : Bool := true) : MetaM (Array TacticDoc) := do let env ← getEnv - let all := - tacticTagExt.toEnvExtension.getState (← getEnv) - |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (← getEnv) (tacticTagExt.getState (← getEnv)) .exported) + let allTags := + tacticTagExt.toEnvExtension.getState env |>.importedEntries + |>.push (tacticTagExt.exportEntriesFn env (tacticTagExt.getState env) .exported) let mut tacTags : NameMap NameSet := {} - for arr in all do + for arr in allTags do for (tac, tag) in arr do tacTags := tacTags.insert tac (tacTags.getD tac {} |>.insert tag) @@ -160,15 +170,18 @@ def allTacticDocs : MetaM (Array TacticDoc) := do let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic | return #[] + + let firstTokens ← firstTacticTokens + for (tac, _) in tactics.kinds do -- Skip noncanonical tactics if let some _ := alternativeOfTactic env tac then continue - let userName : String ← - if let some descr := env.find? tac |>.bind (·.value?) then - if let some tk ← getFirstTk descr then - pure tk.trimAscii.copy - else pure tac.toString - else pure tac.toString + + let userName? : Option String := firstTokens.get? tac + let userName ← + if let some n := userName? then pure n + else if includeUnnamed then pure tac.toString + else continue docs := docs.push { internalName := tac, diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean index f5cac7a9a4..5b170c3d4d 100644 --- a/src/Lean/Parser/Attr.lean +++ b/src/Lean/Parser/Attr.lean @@ -54,7 +54,7 @@ def externEntry := leading_parser nonReservedSymbol "extern" >> many (ppSpace >> externEntry) /-- -Declare this tactic to be an alias or alternative form of an existing tactic. +Declares this tactic to be an alias or alternative form of an existing tactic. This has the following effects: * The alias relationship is saved @@ -64,13 +64,26 @@ This has the following effects: "tactic_alt" >> ppSpace >> ident /-- -Add one or more tags to a tactic. +Adds one or more tags to a tactic. Tags should be applied to the canonical names for tactics. -/ @[builtin_attr_parser] def «tactic_tag» := leading_parser "tactic_tag" >> many1 (ppSpace >> ident) +/-- +Sets the tactic's name. + +Ordinarily, tactic names are automatically set to the first token in the tactic's parser. If this +process fails, or if the tactic's name should be multiple tokens (e.g. `let rec`), then this +attribute can be used to provide a name. + +The tactic's name is used in documentation as well as in completion. Thus, the name should be a +valid prefix of the tactic's syntax. +-/ +@[builtin_attr_parser] def «tactic_name» := leading_parser + "tactic_name" >> ppSpace >> (ident <|> strLit) + end Attr end Lean.Parser diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 0d9bfbd137..d9dc558100 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -52,24 +52,7 @@ example (n : Nat) : n = n := by optional Term.motive >> sepBy1 Term.matchDiscr ", " >> " with " >> ppDedent matchAlts -/-- -The tactic -``` -intro -| pat1 => tac1 -| pat2 => tac2 -``` -is the same as: -``` -intro x -match x with -| pat1 => tac1 -| pat2 => tac2 -``` -That is, `intro` can be followed by match arms and it introduces the values while -doing a pattern match. This is equivalent to `fun` with match arms in term mode. --/ -@[builtin_tactic_parser] def introMatch := leading_parser +@[builtin_tactic_parser, tactic_alt intro] def introMatch := leading_parser nonReservedSymbol "intro" >> matchAlts builtin_initialize diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean index 214e6ac6a8..219f9e2eea 100644 --- a/src/Lean/Parser/Tactic/Doc.lean +++ b/src/Lean/Parser/Tactic/Doc.lean @@ -191,12 +191,13 @@ builtin_initialize unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind let `(«tactic_tag»|tactic_tag $tags*) := stx | throwError "Invalid `[{name}]` attribute syntax" + if (← getEnv).find? decl |>.isSome then if !(isTactic (← getEnv) decl) then - throwErrorAt stx "`{decl}` is not a tactic" + throwErrorAt stx "`{.ofConstName decl}` is not a tactic" if let some tgt' := alternativeOfTactic (← getEnv) decl then - throwErrorAt stx "`{decl}` is an alternative form of `{tgt'}`" + throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`" for t in tags do let tagName := t.getId @@ -271,14 +272,81 @@ where | [l] => " * " ++ l ++ "\n\n" | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n" +/-- +The mapping between tactics and their custom names. + +The first projection in each pair is the tactic name, and the second is the custom name. +-/ +builtin_initialize tacticNameExt + : PersistentEnvExtension + (Name × String) + (Name × String) + (NameMap String) ← + registerPersistentEnvExtension { + mkInitial := pure {}, + addImportedFn := fun _ => pure {}, + addEntryFn := fun as (src, tgt) => as.insert src tgt, + exportEntriesFn := fun es => + es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + } + +/-- +Finds the custom name assigned to `tac`, or returns `none` if there is no such custom name. +-/ +def customTacticName [Monad m] [MonadEnv m] (tac : Name) : m (Option String) := do + let env ← getEnv + match env.getModuleIdxFor? tac with + | some modIdx => + match (tacticNameExt.getModuleEntries env modIdx).binSearch (tac, default) (Name.quickLt ·.1 ·.1) with + | some (_, val) => return some val + | none => return none + | none => return tacticNameExt.getState env |>.find? tac + +builtin_initialize + let name := `tactic_name + registerBuiltinAttribute { + name := name, + ref := by exact decl_name%, + add := fun decl stx kind => do + unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind + let name ← + match stx with + | `(«tactic_name»|tactic_name $name:str) => + pure name.getString + | `(«tactic_name»|tactic_name $name:ident) => + pure (name.getId.toString (escape := false)) + | _ => throwError "Invalid `[{name}]` attribute syntax" + + if (← getEnv).find? decl |>.isSome then + if !(isTactic (← getEnv) decl) then + throwErrorAt stx m!"`{.ofConstName decl}` is not a tactic" + if let some idx := (← getEnv).getModuleIdxFor? decl then + if let some mod := (← getEnv).allImportedModuleNames[idx]? then + throwErrorAt stx m!"`{.ofConstName decl}` is defined in `{mod}`, but custom names can only be added in the tactic's defining module." + else + throwErrorAt stx m!"`{.ofConstName decl}` is defined in an imported module, but custom names can only be added in the tactic's defining module." + + if let some tgt' := alternativeOfTactic (← getEnv) decl then + throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`" + + if let some n ← customTacticName decl then + throwError m!"The tactic `{.ofConstName decl}` already has the custom name `{n}`" + + modifyEnv fun env => tacticNameExt.addEntry env (decl, name) + + descr := + "Registers a custom name for a tactic. This custom name should be a prefix of the " ++ + "tactic's syntax, because it is used in completion.", + applicationTime := .beforeElaboration + } -- Note: this error handler doesn't prevent all cases of non-tactics being added to the data -- structure. But the module will throw errors during elaboration, and there doesn't seem to be -- another way to implement this, because the category parser extension attribute runs *after* the -- attributes specified before a `syntax` command. /-- -Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are -tactics. +Validates that a tactic alternative is actually a tactic, that syntax tagged as tactics are +tactics, and that syntax with tactic names are tactics. -/ private def tacticDocsOnTactics : ParserAttributeHook where postAdd (catName declName : Name) (_builtIn : Bool) := do @@ -291,6 +359,8 @@ private def tacticDocsOnTactics : ParserAttributeHook where if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then if !tags.isEmpty then throwError m!"`{.ofConstName declName}` is not a tactic" + if let some n := tacticNameExt.getState (← getEnv) |>.find? declName then + throwError m!"`{MessageData.ofConstName declName}` is not a tactic, but it was assigned a tactic name `{n}`" builtin_initialize registerParserAttributeHook tacticDocsOnTactics diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 64abd78e47..8dd5aa98da 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -597,7 +597,8 @@ def tacticCompletion (completionInfoPos : Nat) (ctx : ContextInfo) : IO (Array ResolvableCompletionItem) := ctx.runMetaM .empty do - let allTacticDocs ← Tactic.Doc.allTacticDocs + -- Don't include tactics that are identified only by their internal parser name + let allTacticDocs ← Tactic.Doc.allTacticDocs (includeUnnamed := false) let items : Array ResolvableCompletionItem := allTacticDocs.map fun tacticDoc => { label := tacticDoc.userName detail? := none diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index 8aa67b6a41..1d8506cddf 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/src/Std/Tactic/Do/Syntax.lean @@ -290,6 +290,7 @@ syntax "∀" binderIdent : mintroPat @[tactic_alt Lean.Parser.Tactic.mintroMacro] syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic +@[tactic_alt Lean.Parser.Tactic.mintroMacro] macro (name := mintroError) "mintro" : tactic => Macro.throwError "`mintro` expects at least one pattern" macro_rules diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..bbc496d7e7 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,6 @@ #include "util/options.h" +// Dear CI, please update stage0 namespace lean { options get_default_options() { options opts; diff --git a/tests/lean/interactive/completionTactics.lean b/tests/lean/interactive/completionTactics.lean index fed0331571..9477fdc7bc 100644 --- a/tests/lean/interactive/completionTactics.lean +++ b/tests/lean/interactive/completionTactics.lean @@ -118,3 +118,17 @@ example : True := by { skip -- All tactic completions expected } --^ completion + +/-! +Now check that first token detection and tactic names work correctly in completion. +-/ + +/-- Local def -/ +syntax "let " letDecl : tactic + +/-- Local recursive def -/ +@[tactic_name "let rec"] +syntax (name := letrec) "let " &"rec" letRecDecls : tactic + +example : True := by + --^ completion diff --git a/tests/lean/interactive/completionTactics.lean.expected.out b/tests/lean/interactive/completionTactics.lean.expected.out index ea6d6ac564..0e384f50d5 100644 --- a/tests/lean/interactive/completionTactics.lean.expected.out +++ b/tests/lean/interactive/completionTactics.lean.expected.out @@ -4,21 +4,21 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -29,42 +29,35 @@ "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -76,12 +69,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} Resolution of exact: @@ -89,32 +78,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -125,42 +110,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}], "isIncomplete": false} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -172,12 +150,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} Resolution of exact: @@ -185,13 +159,9 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 29, "character": 25}} @@ -199,21 +169,21 @@ Resolution of Lean.Parser.Tactic.introMatch: {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -224,42 +194,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -271,12 +234,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} Resolution of exact: @@ -284,32 +243,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -320,42 +275,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -367,12 +315,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} Resolution of exact: @@ -380,32 +324,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -416,42 +356,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -463,12 +396,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} Resolution of exact: @@ -476,32 +405,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -512,42 +437,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -559,12 +477,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} Resolution of exact: @@ -572,32 +486,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -608,42 +518,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -655,12 +558,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} Resolution of exact: @@ -668,32 +567,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -704,42 +599,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -751,12 +639,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} Resolution of exact: @@ -764,32 +648,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -800,42 +680,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -847,12 +720,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} Resolution of exact: @@ -860,32 +729,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -896,42 +761,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -943,12 +801,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} Resolution of exact: @@ -956,32 +810,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -992,42 +842,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1039,12 +882,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} Resolution of exact: @@ -1052,32 +891,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1088,42 +923,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1135,12 +963,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} Resolution of exact: @@ -1148,13 +972,9 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 81, "character": 4}} @@ -1162,21 +982,21 @@ Resolution of Lean.Parser.Tactic.introMatch: {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1187,42 +1007,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1234,12 +1047,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} Resolution of exact: @@ -1247,32 +1056,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1283,42 +1088,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1330,12 +1128,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} Resolution of exact: @@ -1343,32 +1137,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1379,42 +1169,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1426,12 +1209,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} Resolution of exact: @@ -1439,32 +1218,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1475,42 +1250,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1522,12 +1290,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} Resolution of exact: @@ -1535,13 +1299,9 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 108, "character": 2}} @@ -1549,21 +1309,21 @@ Resolution of Lean.Parser.Tactic.introMatch: {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1574,42 +1334,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1621,12 +1374,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} Resolution of exact: @@ -1634,32 +1383,28 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]} {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 118, "character": 4}} {"items": - [{"label": "Lean.Parser.Tactic.open", + [{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}, - {"label": "Lean.Parser.Tactic.match", + {"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}, - {"label": "Lean.Parser.Tactic.set_option", + {"label": "set_option", "kind": 14, "documentation": {"value": @@ -1670,42 +1415,35 @@ Resolution of Lean.Parser.Tactic.introMatch: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}, - {"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}, - {"label": "Lean.Parser.Tactic.unknown", + {"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}, {"label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}, - {"label": "Lean.Parser.Tactic.introMatch", + {"label": "intro", "kind": 14, - "documentation": - {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", - "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}], "isIncomplete": true} -Resolution of Lean.Parser.Tactic.open: -{"label": "Lean.Parser.Tactic.open", +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} -Resolution of Lean.Parser.Tactic.match: -{"label": "Lean.Parser.Tactic.match", +Resolution of match: +{"label": "match", "kind": 14, "documentation": {"value": "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} -Resolution of Lean.Parser.Tactic.set_option: -{"label": "Lean.Parser.Tactic.set_option", +Resolution of set_option: +{"label": "set_option", "kind": 14, "documentation": {"value": @@ -1717,12 +1455,8 @@ Resolution of skip: "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} -Resolution of Lean.Parser.Tactic.nestedTactic: -{"label": "Lean.Parser.Tactic.nestedTactic", - "kind": 14, - "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} -Resolution of Lean.Parser.Tactic.unknown: -{"label": "Lean.Parser.Tactic.unknown", +Resolution of ident: +{"label": "ident", "kind": 14, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} Resolution of exact: @@ -1730,11 +1464,106 @@ Resolution of exact: "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} -Resolution of Lean.Parser.Tactic.introMatch: -{"label": "Lean.Parser.Tactic.introMatch", +Resolution of intro: +{"label": "intro", + "kind": 14, + "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} +{"textDocument": {"uri": "file:///completionTactics.lean"}, + "position": {"line": 132, "character": 21}} +{"items": + [{"label": "open", + "kind": 14, + "documentation": + {"value": + "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", + "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "match", + "kind": 14, + "documentation": + {"value": + "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", + "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "set_option", + "kind": 14, + "documentation": + {"value": + "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ", + "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "skip", + "kind": 14, + "documentation": {"value": "A docstring ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "ident", + "kind": 14, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "let rec", + "kind": 14, + "documentation": {"value": "Local recursive def ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "exact", + "kind": 14, + "documentation": {"value": "Another docstring ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "intro", + "kind": 14, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}, + {"label": "let", + "kind": 14, + "documentation": {"value": "Local def ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}], + "isIncomplete": true} +Resolution of open: +{"label": "open", "kind": 14, "documentation": {"value": - "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n", + "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ", "kind": "markdown"}, - "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]} + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of match: +{"label": "match", + "kind": 14, + "documentation": + {"value": + "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n match n with\n | 0 => rfl\n | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n", + "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of set_option: +{"label": "set_option", + "kind": 14, + "documentation": + {"value": + "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ", + "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of skip: +{"label": "skip", + "kind": 14, + "documentation": {"value": "A docstring ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of ident: +{"label": "ident", + "kind": 14, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of let rec: +{"label": "let rec", + "kind": 14, + "documentation": {"value": "Local recursive def ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of exact: +{"label": "exact", + "kind": 14, + "documentation": {"value": "Another docstring ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of intro: +{"label": "intro", + "kind": 14, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} +Resolution of let: +{"label": "let", + "kind": 14, + "documentation": {"value": "Local def ", "kind": "markdown"}, + "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]} diff --git a/tests/lean/run/tacticDoc.lean b/tests/lean/run/tacticDoc.lean index 081ad4fbdf..76c7e3515a 100644 --- a/tests/lean/run/tacticDoc.lean +++ b/tests/lean/run/tacticDoc.lean @@ -128,17 +128,78 @@ Note: This linter can be disabled with `set_option linter.tactic.docsOnAlt false attribute [tactic_alt my_trivial] «yetAnother» /-! # Querying Tactic Docs -/ + +/-! +`tm` is part of the below set because the tag attribute can't reject `someTerm` above before it is +added. Because it's not a tactic, its first token is not found. +-/ + /-- info: Available tags: ⏎ • `ctrl` — "control flow" Tactics that sequence or arrange other tactics ⏎ - '<;>' + `<;>` • `extensible` Tactics that are intended to be extensible ⏎ - 'my_trivial' + `my_trivial` • `finishing` Finishing tactics that are intended to completely close a goal ⏎ - 'omega', 'my_trivial', 'someTerm' + `omega`, `my_trivial`, `tm` -/ #guard_msgs in #print tactic tags + +/-! +## Custom Names + +The next two tests check that custom tactic names are shown. +-/ +@[tactic_tag finishing] +syntax (name := fooBar) "foo" "bar" term : tactic + + +/-! +Here, the first token `foo` is shown: +-/ +/-- +info: Available tags: ⏎ + • `ctrl` — "control flow" + Tactics that sequence or arrange other tactics ⏎ + `<;>` + • `extensible` + Tactics that are intended to be extensible ⏎ + `my_trivial` + • `finishing` + Finishing tactics that are intended to completely close a goal ⏎ + `omega`, `foo`, `my_trivial`, `tm` +-/ +#guard_msgs in +#print tactic tags + +attribute [tactic_name "foo bar"] fooBar + +/-! +Now we show `foo bar`: +-/ +/-- +info: Available tags: ⏎ + • `ctrl` — "control flow" + Tactics that sequence or arrange other tactics ⏎ + `<;>` + • `extensible` + Tactics that are intended to be extensible ⏎ + `my_trivial` + • `finishing` + Finishing tactics that are intended to completely close a goal ⏎ + `omega`, `foo bar`, `my_trivial`, `tm` +-/ +#guard_msgs in +#print tactic tags + +/-! +This test checks that tactic names can't be added to other kinds of syntax. +-/ +/-- error: `termNotATactic` is not a tactic, but it was assigned a tactic name `t` -/ +#guard_msgs in +@[tactic_name t] +syntax "not " "a " "tactic" : term diff --git a/tests/lean/run/tacticDocAllModule.lean b/tests/lean/run/tacticDocAllModule.lean new file mode 100644 index 0000000000..6257e28e6e --- /dev/null +++ b/tests/lean/run/tacticDocAllModule.lean @@ -0,0 +1,25 @@ +module + +import Lean.Elab.Tactic.Doc + +/-! +This test checks that the first tokens are found for the tactics that ship with Lean when in a +module. + +In the past, the first token detection code attempted to process the descriptor in the environment; +this failed in modules because the parser was not loaded. This test, along with tacticDocAllNonmod, +check that the code works correctly both in and out of modules. +-/ + +open Lean.Elab.Tactic.Doc + +#guard_msgs in +open Lean in +#eval do + let docs ← allTacticDocs + let userNames := docs.map TacticDoc.userName + if userNames.size < 50 then + throwError "Implausibly few user names found: {userNames}" + for n in userNames do + if n.startsWith "Lean.Parser.Tactic" && n ≠ "Lean.Parser.Tactic.nestedTactic" then + logError "Didn't find a first token for tactic parser {n}" diff --git a/tests/lean/run/tacticDocAllNonmod.lean b/tests/lean/run/tacticDocAllNonmod.lean new file mode 100644 index 0000000000..804b80b5b4 --- /dev/null +++ b/tests/lean/run/tacticDocAllNonmod.lean @@ -0,0 +1,23 @@ +import Lean.Elab.Tactic.Doc + +/-! +This test checks that the first tokens are found for the tactics that ship with Lean when not in a +module. + +In the past, the first token detection code attempted to process the descriptor in the environment; +this failed in modules because the parser was not loaded. This test, along with tacticDocAllModule, +check that the code works correctly both in and out of modules. +-/ + +open Lean.Elab.Tactic.Doc + +#guard_msgs in +open Lean in +#eval do + let docs ← allTacticDocs + let userNames := docs.map TacticDoc.userName + if userNames.size < 50 then + throwError "Implausibly few user names found: {userNames}" + for n in userNames do + if n.startsWith "Lean.Parser.Tactic" && n ≠ "Lean.Parser.Tactic.nestedTactic" then + logError "Didn't find a first token for tactic parser {n}" diff --git a/tests/lean/run/tacticDocUserName.lean b/tests/lean/run/tacticDocUserName.lean new file mode 100644 index 0000000000..682ac402e7 --- /dev/null +++ b/tests/lean/run/tacticDocUserName.lean @@ -0,0 +1,61 @@ +import Lean + +open Lean Elab Tactic Doc + +/-! +This test ensures that user-facing tactic names shipped with Lean are kept unambiguous. +-/ +#eval show MetaM Unit from do + let firsts ← firstTacticTokens + + -- Compute a reverse mapping from first tokens to their syntax kinds + let mut rev : Std.HashMap String (List Name) := {} + for (k, firstTok) in firsts do + rev := rev.alter firstTok fun x? => x?.map (k :: ·) |>.getD [k] + + -- Check each for ambiguity + for (firstTok, kindsForToken) in rev do + + -- Skip kinds that are alternative syntax for some user-facing parser + let kindsForToken ← kindsForToken.filterM fun k => do + pure <| (Parser.Tactic.Doc.alternativeOfTactic (← getEnv) k).isNone + + -- Until a stage0 update allows let rec to have a custom name, ignore it. Then update this test. + let kindsForToken := kindsForToken.filter (· ≠ ``Lean.Parser.Tactic.letrec) + if firstTok.contains ' ' then throwError "Test needs updating after stage0 update (see comment)" + + -- If it's ambiguous, log an error. + if kindsForToken.length > 1 then + let kinds := MessageData.andList <| kindsForToken.map (m!"`{.ofConstName ·}`") + logError m!"`{firstTok}` is the ambiguous first token for {kinds}" + +/-! +This test ensures that user-facing tactic names are found for all the tactics that we ship. +-/ +#eval show MetaM Unit from do + let firsts ← firstTacticTokens + let some tactics := (Lean.Parser.parserExtension.getState (← getEnv)).categories.find? `tactic + | return + for (t, ()) in tactics.kinds do + if t == ``Lean.Parser.Tactic.nestedTactic then continue + unless firsts.contains t do + logError m!"Couldn't find the first token for tactic syntax kind {t}" + +/-! +This test spot-checks tactics defined in a few ways to make sure they all have user-facing names: + * Defined using `syntax ... : tactic`, both leading and trailing (`intros` and `<;>`) + * Defined using `declare_simp_like_tactic` (`simpAutoUnfold`) + * Defined with custom user-facing names (`Lean.Parser.Tactic.letrec`) (after stage0 update) +-/ +/-- +info: (some intro) +(some <;>) +(some simp!) +-/ +#guard_msgs in +#eval show MetaM Unit from do + let firsts ← firstTacticTokens + IO.println (firsts.get? ``Lean.Parser.Tactic.intro) + IO.println (firsts.get? ``Lean.Parser.Tactic.«tactic_<;>_») + IO.println (firsts.get? ``Lean.Parser.Tactic.simpAutoUnfold) + --IO.println (firsts.get? ``Lean.Parser.Tactic.letrec)