From e0ce2e645614a28fcb7a8d07e13110ca61a8b846 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 30 Jan 2025 15:58:33 +0100 Subject: [PATCH 1/6] feat: `recommended_spelling` command --- src/Lean/DocString.lean | 5 +- src/Lean/Elab.lean | 1 + src/Lean/Elab/RecommendedSpelling.lean | 34 ++++++++++ src/Lean/Parser/Command.lean | 24 +++++++ src/Lean/Parser/Term.lean | 1 + src/Lean/Parser/Term/Doc.lean | 83 +++++++++++++++++++++++++ tests/lean/run/recommendedSpelling.lean | 64 +++++++++++++++++++ 7 files changed, 211 insertions(+), 1 deletion(-) create mode 100644 src/Lean/Elab/RecommendedSpelling.lean create mode 100644 src/Lean/Parser/Term/Doc.lean create mode 100644 tests/lean/run/recommendedSpelling.lean diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean index d28822820955..15c0fb12b265 100644 --- a/src/Lean/DocString.lean +++ b/src/Lean/DocString.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.DocString.Extension import Lean.Parser.Tactic.Doc +import Lean.Parser.Term.Doc set_option linter.missingDocs true @@ -15,6 +16,7 @@ set_option linter.missingDocs true namespace Lean open Lean.Parser.Tactic.Doc +open Lean.Parser.Term.Doc /-- Finds the docstring for a name, taking tactic alternate forms and documentation extensions into @@ -26,4 +28,5 @@ including extensions. def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do let declName := alternativeOfTactic env declName |>.getD declName let exts := getTacticExtensionString env declName - return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts) + let spellings := getRecommendedSpellingString env declName + return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts ++ spellings) diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index 9f0ee920281d..8f7256783214 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -54,3 +54,4 @@ import Lean.Elab.CheckTactic import Lean.Elab.MatchExpr import Lean.Elab.Tactic.Doc import Lean.Elab.Time +import Lean.Elab.RecommendedSpelling diff --git a/src/Lean/Elab/RecommendedSpelling.lean b/src/Lean/Elab/RecommendedSpelling.lean new file mode 100644 index 000000000000..11a8e53ccfe7 --- /dev/null +++ b/src/Lean/Elab/RecommendedSpelling.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Lean.Parser.Term.Doc +import Lean.Parser.Command +import Lean.Elab.Command + +namespace Lean.Elab.Term.Doc +open Lean.Parser.Term.Doc +open Lean.Elab.Command +open Lean.Parser.Command + +@[builtin_command_elab «recommended_spelling»] def elabRecommendedSpelling : CommandElab + | `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $notation_:str $spelling:str $decls*) => do + let declNames ← liftTermElabM <| decls.mapM (fun decl => realizeGlobalConstNoOverloadWithInfo decl) + let recommendedSpelling : RecommendedSpelling := { + notation_ := notation_.getString + recommendedSpelling := spelling.getString + additionalInformation? := docs.map (·.getDocString) + } + modifyEnv (addRecommendedSpelling · recommendedSpelling declNames) + | _ => throwError "Malformed recommended spelling command" + +/-- Returns an array containing all recommended spellings. -/ +def allRecommendedSpellings : MetaM (Array RecommendedSpelling) := do + let all := recommendedSpellingExt.toEnvExtension.getState (← getEnv) + |>.importedEntries + |>.push (recommendedSpellingExt.exportEntriesFn (recommendedSpellingExt.getState (← getEnv))) + return all.flatMap id + +end Lean.Elab.Term.Doc diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 73a94a5b0fae..f581d2c23302 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -754,6 +754,30 @@ list, so it should be brief. optional (docComment >> ppLine) >> "tactic_extension " >> ident +/-- +Document a recommended spelling for a notation in identifiers. + +``` +/-- some additional info -/ +recommended_spelling "∧" "and" And «term_∧_» +``` + +will do the following: +* Adds the sentence "The recommended spelling of `∧` in identifier is `and` (some additional info)." + to the end of the docstring for `And` and for `∧`. If the additional info is more than a single + line, it will be placed below the sentence instead of in parentheses. +* Registers this information in an environment extension, so that it will later be possible to + generate a table with all recommended spellings. + +You can add attach the recommended spelling to as many declarations as you want. It is recommended +to attach the recommended spelling to all relevant parsers as well as the declaration the parsers +refer to (if such a declaration exists). Note that the `inherit_doc` attribute does *not* copy +recommended spellings, so even though the parser for `∧` uses `@[inherit_doc And]`, we have to +attach the recommended spelling to both `And` and `«term_∧_»`. +-/ +@[builtin_command_parser] def «recommended_spelling» := leading_parser + optional (docComment >> ppLine) >> + "recommended_spelling " >> strLit >> ppSpace >> strLit >> ppSpace >> many1 ident /-- This is an auxiliary command for generation constructor injectivity theorems for diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 639b534e76e9..7014ff76c77a 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro prelude import Lean.Parser.Attr import Lean.Parser.Level +import Lean.Parser.Term.Doc namespace Lean namespace Parser diff --git a/src/Lean/Parser/Term/Doc.lean b/src/Lean/Parser/Term/Doc.lean new file mode 100644 index 000000000000..200a7e36b3ed --- /dev/null +++ b/src/Lean/Parser/Term/Doc.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Lean.Parser.Extension + +/-! Environment extension to register preferred spellings of notations in identifiers. -/ + +set_option linter.missingDocs true + +namespace Lean.Parser.Term.Doc + +/-- Information about how to spell a certain notation for an identifier in declaration names. -/ +structure RecommendedSpelling where + /-- The notation in question. -/ + notation_ : String + /-- The recommended spelling of the notation in identifiers. -/ + recommendedSpelling : String + /-- Additional information. -/ + additionalInformation? : Option String + +/-- +Recommended spellings for notations, stored in a way so that the recommended spellings for a given +declaration are easily accessible. +-/ +builtin_initialize recommendedSpellingByNameExt + : PersistentEnvExtension (Name × Array RecommendedSpelling) (RecommendedSpelling × Array Name) + (NameMap (Array RecommendedSpelling)) ← + registerPersistentEnvExtension { + mkInitial := pure {}, + addImportedFn := fun _ => pure {}, + addEntryFn := fun es (rec, xs) => xs.foldl (init := es) fun es x => es.insert x (es.findD x #[] |>.push rec), + exportEntriesFn := fun es => + es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + } + +/-- Recommended spellings for notations, stored in such a way that it is easy to generate a table +containing every recommended spelling exactly once. -/ +builtin_initialize recommendedSpellingExt + : PersistentEnvExtension RecommendedSpelling RecommendedSpelling (Array RecommendedSpelling) ← + registerPersistentEnvExtension { + mkInitial := pure {}, + addImportedFn := fun _ => pure {}, + addEntryFn := Array.push, + exportEntriesFn := id + } + +/-- Adds a recommended spelling to the environment. -/ +def addRecommendedSpelling (env : Environment) (rec : RecommendedSpelling) (names : Array Name) : Environment := + let env := recommendedSpellingExt.addEntry env rec + recommendedSpellingByNameExt.addEntry env (rec, names) + +/-- Returns the recommended spellings associated with the given declaration name. -/ +def getRecommendedSpellingsForName (env : Environment) (declName : Name) : + Array RecommendedSpelling := Id.run do + let mut spellings := #[] + for modArr in recommendedSpellingByNameExt.toEnvExtension.getState env |>.importedEntries do + if let some (_, strs) := modArr.binSearch (declName, #[]) (Name.quickLt ·.1 ·.1) then + spellings := spellings ++ strs + if let some strs := recommendedSpellingByNameExt.getState env |>.find? declName then + spellings := spellings ++ strs + return spellings + +/-- Renders the recommended spellings for the given declaration into a string for appending to +the docstring. -/ +def getRecommendedSpellingString (env : Environment) (declName : Name) : String := Id.run do + let spellings := getRecommendedSpellingsForName env declName + if spellings.size == 0 then "" + else "\n\nConventions for notations in identifiers:\n\n" ++ String.join (spellings.toList.map bullet) |>.trimRight +where + indentLine (str : String) : String := + (if str.all (·.isWhitespace) then str else " " ++ str) ++ "\n" + bullet (spelling : RecommendedSpelling) : String := + let firstLine := s!"* The recommended spelling of `{spelling.notation_}` in identifiers is `{spelling.recommendedSpelling}`" + let additionalInfoLines := spelling.additionalInformation?.map (·.splitOn "\n") + match additionalInfoLines with + | none | some [] => firstLine ++ ".\n\n" + | some [l] => firstLine ++ s!" ({l.trimRight}).\n\n" + | some ls => firstLine ++ ".\n\n" ++ String.join (ls.map indentLine) ++ "\n\n" + +end Lean.Parser.Term.Doc diff --git a/tests/lean/run/recommendedSpelling.lean b/tests/lean/run/recommendedSpelling.lean new file mode 100644 index 000000000000..c4ff58f3b400 --- /dev/null +++ b/tests/lean/run/recommendedSpelling.lean @@ -0,0 +1,64 @@ +import Lean + +/-! +Test the `recommended_spelling` command. + +TODO: once we use this command in Init, we can test that recommended spellings from imported +modules are reported correctly. +-/ + +/-- +Conjuction + +Second line +-/ +inductive MyAnd (P Q : Prop) : Prop where + | intro : P → Q → MyAnd P Q + +@[inherit_doc] infixr:35 " ☃ " => MyAnd +@[inherit_doc] infixr:35 " ☋ " => MyAnd + +recommended_spelling "☃" "snowmand" MyAnd «term_☃_» +/-- the preferred notation is `∧`. + +more stuff + +even more stuff + +hello + +-/ +recommended_spelling "☋" "orbitalAnd" MyAnd «term_☋_» +/-- Docstring -/ +recommended_spelling "something" "and" And «term_☃_» «term_☋_» + +def findDocString? (n : Lean.Name) : Lean.MetaM (Option String) := do + Lean.findDocString? (← Lean.getEnv) n + +/-- +info: some + "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n* The recommended spelling of `☃` in identifiers is `snowmand`.\n\n* The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello" +-/ +#guard_msgs in +#eval findDocString? `MyAnd + +/-- +info: some + "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n* The recommended spelling of `☃` in identifiers is `snowmand`.\n\n* The recommended spelling of `something` in identifiers is `and` (Docstring)." +-/ +#guard_msgs in +#eval findDocString? `«term_☃_» + +/-- +info: some + "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n* The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello\n\n\n\n\n* The recommended spelling of `something` in identifiers is `and` (Docstring)." +-/ +#guard_msgs in +#eval findDocString? `«term_☋_» + +/-- info: 1 -/ +#guard_msgs in +#eval do + return (← Lean.Elab.Term.Doc.allRecommendedSpellings) + |>.map Lean.Parser.Term.Doc.RecommendedSpelling.notation_ + |>.count "☋" From 9499b138cf7387b35482cb42eb28d9d7abae4b91 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 30 Jan 2025 16:15:47 +0100 Subject: [PATCH 2/6] fix test --- tests/lean/run/recommendedSpelling.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/recommendedSpelling.lean b/tests/lean/run/recommendedSpelling.lean index c4ff58f3b400..496b1d7e5b73 100644 --- a/tests/lean/run/recommendedSpelling.lean +++ b/tests/lean/run/recommendedSpelling.lean @@ -30,7 +30,7 @@ hello -/ recommended_spelling "☋" "orbitalAnd" MyAnd «term_☋_» /-- Docstring -/ -recommended_spelling "something" "and" And «term_☃_» «term_☋_» +recommended_spelling "something" "and" «term_☃_» «term_☋_» def findDocString? (n : Lean.Name) : Lean.MetaM (Option String) := do Lean.findDocString? (← Lean.getEnv) n From b03a38252b682d4da1d22a44fdebbea8c6fbfead Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 31 Jan 2025 15:17:18 +0100 Subject: [PATCH 3/6] Apply suggestions from code review --- src/Lean/Elab/RecommendedSpelling.lean | 4 ++-- src/Lean/Parser/Command.lean | 14 +++++++++----- src/Lean/Parser/Term/Doc.lean | 4 ++-- tests/lean/run/recommendedSpelling.lean | 4 ++-- 4 files changed, 15 insertions(+), 11 deletions(-) diff --git a/src/Lean/Elab/RecommendedSpelling.lean b/src/Lean/Elab/RecommendedSpelling.lean index 11a8e53ccfe7..5657f3023951 100644 --- a/src/Lean/Elab/RecommendedSpelling.lean +++ b/src/Lean/Elab/RecommendedSpelling.lean @@ -14,10 +14,10 @@ open Lean.Elab.Command open Lean.Parser.Command @[builtin_command_elab «recommended_spelling»] def elabRecommendedSpelling : CommandElab - | `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $notation_:str $spelling:str $decls*) => do + | `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $spelling:str for $«notation»:str in [$[$decls:ident],*]) => do let declNames ← liftTermElabM <| decls.mapM (fun decl => realizeGlobalConstNoOverloadWithInfo decl) let recommendedSpelling : RecommendedSpelling := { - notation_ := notation_.getString + «notation» := «notation».getString recommendedSpelling := spelling.getString additionalInformation? := docs.map (·.getDocString) } diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index f581d2c23302..0945087cf10f 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -736,7 +736,7 @@ Documentation can only be added to declarations in the same module. docComment >> "add_decl_doc " >> ident /-- -Register a tactic tag, saving its user-facing name and docstring. +Registers a tactic tag, saving its user-facing name and docstring. Tactic tags can be used by documentation generation tools to classify related tactics. -/ @@ -745,7 +745,7 @@ Tactic tags can be used by documentation generation tools to classify related ta "register_tactic_tag " >> ident >> strLit /-- -Add more documentation as an extension of the documentation for a given tactic. +Adds more documentation as an extension of the documentation for a given tactic. The extended documentation is placed in the command's docstring. It is shown as part of a bulleted list, so it should be brief. @@ -755,7 +755,10 @@ list, so it should be brief. "tactic_extension " >> ident /-- -Document a recommended spelling for a notation in identifiers. +Documents a recommended spelling for a notation in identifiers. + +Theorems should generally be systematically named after their statement, rather than creatively. +Non-identifier notations should be referred to consistently by their recommended spelling. ``` /-- some additional info -/ @@ -763,7 +766,7 @@ recommended_spelling "∧" "and" And «term_∧_» ``` will do the following: -* Adds the sentence "The recommended spelling of `∧` in identifier is `and` (some additional info)." +* Adds the sentence "The recommended spelling of `∧` in identifiers is `and` (some additional info)." to the end of the docstring for `And` and for `∧`. If the additional info is more than a single line, it will be placed below the sentence instead of in parentheses. * Registers this information in an environment extension, so that it will later be possible to @@ -777,7 +780,8 @@ attach the recommended spelling to both `And` and `«term_∧_»`. -/ @[builtin_command_parser] def «recommended_spelling» := leading_parser optional (docComment >> ppLine) >> - "recommended_spelling " >> strLit >> ppSpace >> strLit >> ppSpace >> many1 ident + "recommended_spelling " >> strLit >> " for " >> strLit >> " in " >> + "[" >> sepBy1 ident ", " >> "]" /-- This is an auxiliary command for generation constructor injectivity theorems for diff --git a/src/Lean/Parser/Term/Doc.lean b/src/Lean/Parser/Term/Doc.lean index 200a7e36b3ed..d4305fdd27fe 100644 --- a/src/Lean/Parser/Term/Doc.lean +++ b/src/Lean/Parser/Term/Doc.lean @@ -15,7 +15,7 @@ namespace Lean.Parser.Term.Doc /-- Information about how to spell a certain notation for an identifier in declaration names. -/ structure RecommendedSpelling where /-- The notation in question. -/ - notation_ : String + «notation» : String /-- The recommended spelling of the notation in identifiers. -/ recommendedSpelling : String /-- Additional information. -/ @@ -73,7 +73,7 @@ where indentLine (str : String) : String := (if str.all (·.isWhitespace) then str else " " ++ str) ++ "\n" bullet (spelling : RecommendedSpelling) : String := - let firstLine := s!"* The recommended spelling of `{spelling.notation_}` in identifiers is `{spelling.recommendedSpelling}`" + let firstLine := s!" * The recommended spelling of `{spelling.«notation»}` in identifiers is `{spelling.recommendedSpelling}`" let additionalInfoLines := spelling.additionalInformation?.map (·.splitOn "\n") match additionalInfoLines with | none | some [] => firstLine ++ ".\n\n" diff --git a/tests/lean/run/recommendedSpelling.lean b/tests/lean/run/recommendedSpelling.lean index 496b1d7e5b73..17be79a861b9 100644 --- a/tests/lean/run/recommendedSpelling.lean +++ b/tests/lean/run/recommendedSpelling.lean @@ -18,7 +18,7 @@ inductive MyAnd (P Q : Prop) : Prop where @[inherit_doc] infixr:35 " ☃ " => MyAnd @[inherit_doc] infixr:35 " ☋ " => MyAnd -recommended_spelling "☃" "snowmand" MyAnd «term_☃_» +recommended_spelling "snowmand" for "☃" in [MyAnd, «term_☃_»] /-- the preferred notation is `∧`. more stuff @@ -60,5 +60,5 @@ info: some #guard_msgs in #eval do return (← Lean.Elab.Term.Doc.allRecommendedSpellings) - |>.map Lean.Parser.Term.Doc.RecommendedSpelling.notation_ + |>.map Lean.Parser.Term.Doc.RecommendedSpelling.«notation» |>.count "☋" From 4e26674eb133fb2d054aad0457546431fc208bf3 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 31 Jan 2025 15:18:15 +0100 Subject: [PATCH 4/6] Fix tests and documentation --- src/Lean/Parser/Command.lean | 2 +- tests/lean/run/recommendedSpelling.lean | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 0945087cf10f..27ecf505fea3 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -762,7 +762,7 @@ Non-identifier notations should be referred to consistently by their recommended ``` /-- some additional info -/ -recommended_spelling "∧" "and" And «term_∧_» +recommended_spelling "and" for "∧" in [And, «term_∧_»] ``` will do the following: diff --git a/tests/lean/run/recommendedSpelling.lean b/tests/lean/run/recommendedSpelling.lean index 17be79a861b9..d62ba1d4762a 100644 --- a/tests/lean/run/recommendedSpelling.lean +++ b/tests/lean/run/recommendedSpelling.lean @@ -28,30 +28,30 @@ even more stuff hello -/ -recommended_spelling "☋" "orbitalAnd" MyAnd «term_☋_» +recommended_spelling "orbitalAnd" for "☋" in [MyAnd, «term_☋_»] /-- Docstring -/ -recommended_spelling "something" "and" «term_☃_» «term_☋_» +recommended_spelling "and" for "something" in [«term_☃_», «term_☋_»] def findDocString? (n : Lean.Name) : Lean.MetaM (Option String) := do Lean.findDocString? (← Lean.getEnv) n /-- info: some - "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n* The recommended spelling of `☃` in identifiers is `snowmand`.\n\n* The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello" + "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☃` in identifiers is `snowmand`.\n\n * The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello" -/ #guard_msgs in #eval findDocString? `MyAnd /-- info: some - "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n* The recommended spelling of `☃` in identifiers is `snowmand`.\n\n* The recommended spelling of `something` in identifiers is `and` (Docstring)." + "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☃` in identifiers is `snowmand`.\n\n * The recommended spelling of `something` in identifiers is `and` (Docstring)." -/ #guard_msgs in #eval findDocString? `«term_☃_» /-- info: some - "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n* The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello\n\n\n\n\n* The recommended spelling of `something` in identifiers is `and` (Docstring)." + "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello\n\n\n\n\n * The recommended spelling of `something` in identifiers is `and` (Docstring)." -/ #guard_msgs in #eval findDocString? `«term_☋_» From e10ab6088c80a1bf9235a2f62428f4b9ce732c38 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sat, 1 Feb 2025 08:18:08 +0100 Subject: [PATCH 5/6] Improve command documentation as discussed in code review --- src/Lean/Parser/Command.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 27ecf505fea3..6f00363a01f3 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -777,6 +777,10 @@ to attach the recommended spelling to all relevant parsers as well as the declar refer to (if such a declaration exists). Note that the `inherit_doc` attribute does *not* copy recommended spellings, so even though the parser for `∧` uses `@[inherit_doc And]`, we have to attach the recommended spelling to both `And` and `«term_∧_»`. + +The `syntax`, `macro`, `elab` and `notation` commands accept a `(name := parserName)` option to +assign a name to the created parser so that you do not have to guess the automatically generated +name. The `synax`, `macro` and `elab` commands can be hovered to see the name of the parser. -/ @[builtin_command_parser] def «recommended_spelling» := leading_parser optional (docComment >> ppLine) >> @@ -790,6 +794,13 @@ attach the recommended spelling to both `And` and `«term_∧_»`. @[builtin_command_parser] def genInjectiveTheorems := leading_parser "gen_injective_theorems% " >> ident + +notation (name := bluib) a " andaa " b => a ∧ b + +#check True andaa True + +#check aa + /-- `include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all theorems in the remainder of the current section, differing from the default behavior of From 3326ff7086139b8f4851483f7bcdcc65d3263875 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sat, 1 Feb 2025 08:19:08 +0100 Subject: [PATCH 6/6] I should get a VS Code extension that warns you if you commit a file that has unsaved changes --- src/Lean/Parser/Command.lean | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 6f00363a01f3..2a3808a84120 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -781,6 +781,15 @@ attach the recommended spelling to both `And` and `«term_∧_»`. The `syntax`, `macro`, `elab` and `notation` commands accept a `(name := parserName)` option to assign a name to the created parser so that you do not have to guess the automatically generated name. The `synax`, `macro` and `elab` commands can be hovered to see the name of the parser. + +For complex notations which enclose identifiers, the convention is to use example identifiers rather +than other placeholders. This is an example following the convention: +``` +recommended_spelling "singleton" for "[a]" in [List.cons, «term[_]»] +``` +Using `[·]` or `[⋯]` or `[…]` instead of `[a]` would be against the convention. When attaching a +recommended spelling to a notation whose docstring already has an example, try to reuse the +identifier names chosen in the docstring for consistency. -/ @[builtin_command_parser] def «recommended_spelling» := leading_parser optional (docComment >> ppLine) >> @@ -794,13 +803,6 @@ name. The `synax`, `macro` and `elab` commands can be hovered to see the name of @[builtin_command_parser] def genInjectiveTheorems := leading_parser "gen_injective_theorems% " >> ident - -notation (name := bluib) a " andaa " b => a ∧ b - -#check True andaa True - -#check aa - /-- `include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all theorems in the remainder of the current section, differing from the default behavior of