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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `10061bf49d6d842b2099878901410ef3b6a393c2`
+Mathlib version: `a8071348b19ed841a1f46dbd5a25d109bc804711`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `10061bf49d6d842b2099878901410ef3b6a393c2`
+Mathlib version: `a8071348b19ed841a1f46dbd5a25d109bc804711`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `10061bf49d6d842b2099878901410ef3b6a393c2`
+Mathlib version: `a8071348b19ed841a1f46dbd5a25d109bc804711`
 
 ## Elab.async
 type: `Bool`
@@ -1220,6 +1220,13 @@ default: `32`
 
 maximum universe level offset
 
+## max_memory
+type: `Nat`
+
+default: `0`
+
+
+
 ## moogle.queries
 type: `Nat`
 
@@ -1885,7 +1892,7 @@ Number of results requested from statesearch (default 6)
 ## statesearch.revision
 type: `String`
 
-default: `"v4.23.0-rc2"`
+default: `"v4.23.0"`
 
 Revision of LeanStateSearch to use
 
@@ -1973,6 +1980,13 @@ default: `true`
 
 in the `rw` and `simp` tactics, if an instance implicit argument is assigned, do not try to synthesize instance.
 
+## timeout
+type: `Nat`
+
+default: `0`
+
+
+
 ## trace.Aesop.Util.EqualUpToIds
 type: `Bool`
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `10061bf49d6d842b2099878901410ef3b6a393c2`
+Mathlib version: `a8071348b19ed841a1f46dbd5a25d109bc804711`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "10061bf49d6d842b2099878901410ef3b6a393c2",
+   "rev": "a8071348b19ed841a1f46dbd5a25d109bc804711",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
+   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7c02243c07b61d493d7607ede432026781a3e47c",
+   "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
+   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
+   "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a9a0cb7672b7134497c9d813e53999c9311f4037",
+   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
+   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.23.0-rc2
+leanprover/lean4:v4.23.0