Merge pull request #553 from Seasawher/auto-update-branch

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `790901a8c97c730ae7af9bd44fe60c733a21d9ba`
+Mathlib version: `d0cc8265b663c197e6500917efd4383278cf073e`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `790901a8c97c730ae7af9bd44fe60c733a21d9ba`
+Mathlib version: `d0cc8265b663c197e6500917efd4383278cf073e`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`
@@ -1992,31 +1992,44 @@ a theorem `foo_def : foo = 42`.
 ## library_note
 Defined in: `Batteries.Util.LibraryNote.commandLibrary_note___`
 
-```
-library_note "some tag" /--
-... some explanation ...
--/
-```
-creates a new "library note", which can then be cross-referenced using
+`library_note «my note» /-- documentation -/` creates a library note named `my note`
+in the `LibraryNote` namespace, whose content is `/-- documentation -/`.
+This can then be cross-referenced using
 ```
 -- See note [some tag]
 ```
 in doc-comments.
+You can access the contents using, for example, `#print LibraryNote.«my note»`.
 Use `#help note "some tag"` to display all notes with the tag `"some tag"` in the infoview.
 This command can be imported from Batteries.Tactic.HelpCmd .
 
+## library_note
+Defined in: `Batteries.Util.LibraryNote.commandLibrary_note____1`
+
+Support the old `library_note "foo"` syntax, with a deprecation warning.
+
 ## library_note2
 Defined in: `commandLibrary_note2____1`
 
 Support the old `library_note "foo"` syntax, with a deprecation warning.
 
+## library_note2
+Defined in: `Batteries.Util.LibraryNote.commandLibrary_note2___`
+
+Support the old `library_note2 «foo»` syntax, with a deprecation warning.
+
 ## library_note2
 Defined in: `commandLibrary_note2___`
 
 `library_note2 «my note» /-- documentation -/` creates a library note named `my note`
 in the `Mathlib.LibraryNote` namespace, whose content is `/-- documentation -/`.
 You can access this note using, for example, `#print Mathlib.LibraryNote.«my note»`.
 
+## library_note2
+Defined in: `Batteries.Util.LibraryNote.commandLibrary_note2____1`
+
+Support the old `library_note2 "foo"` syntax, with a deprecation warning.
+
 ## lrat_proof
 Defined in: `Mathlib.Tactic.Sat.commandLrat_proof_Example____`
 

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `790901a8c97c730ae7af9bd44fe60c733a21d9ba`
+Mathlib version: `d0cc8265b663c197e6500917efd4383278cf073e`
 
 ## Elab.async
 type: `Bool`
@@ -890,6 +890,13 @@ default: `false`
 
 
 
+## linter.nonbreakingSpace
+type: `Bool`
+
+default: `true`
+
+
+
 ## linter.oldObtain
 type: `Bool`
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `790901a8c97c730ae7af9bd44fe60c733a21d9ba`
+Mathlib version: `d0cc8265b663c197e6500917efd4383278cf073e`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "790901a8c97c730ae7af9bd44fe60c733a21d9ba",
+   "rev": "d0cc8265b663c197e6500917efd4383278cf073e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f2aca6fc4a47c5b67fad08d3eda5e949d5b73ac0",
+   "rev": "44cdfa76dc744fb0cd356457dcdcc5366ec647ac",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",