generated by GitHub Action

Author: actions-user

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
+Mathlib version: `80732f7660133e80dc57657649e7e09584749454`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
+Mathlib version: `80732f7660133e80dc57657649e7e09584749454`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`
@@ -2122,7 +2122,9 @@ 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»`.
+You can access the contents using, for example, `#print LibraryNote.my_note`.
+(Note: spaces in the name are converted to underscores in the declaration name for
+compatibility with the Lean export format.)
 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 .
 

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
+Mathlib version: `80732f7660133e80dc57657649e7e09584749454`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
+Mathlib version: `80732f7660133e80dc57657649e7e09584749454`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "98379c78c5dd2e3614cd24ab7ad22f5713e0eb63",
+   "rev": "80732f7660133e80dc57657649e7e09584749454",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eff6c5186ebd4dd594eda5b169aef9a55a8b6d2",
+   "rev": "5ba0380f2fb45c69448d80429ef6c22bf5973cfa",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",