Bump to nightly-2023-08-17

AesopTest/List.lean

@@ -89,6 +89,7 @@ instance : Membership α (Option α) :=
 
 @[simp]
 theorem mem_spec {o : Option α} : a ∈ o ↔ o = some a := by
+ set_option aesop.check.script false in -- TODO
  aesop (add norm simp Membership.mem)
 
 @[simp]
@@ -305,6 +306,7 @@ theorem mem_map_of_injective {f : α → β} (H : Injective f) {a : α} {l : Lis
 @[simp] theorem _root_.function.involutive.exists_mem_and_apply_eq_iff {f : α → α}
  (hf : Involutive f) (x : α) (l : List α) :
  (∃ (y : α), y ∈ l ∧ f y = x) ↔ f x ∈ l := by
+ set_option aesop.check.script false in -- TODO
  aesop
 
 theorem mem_map_of_involutive {f : α → α} (hf : Involutive f) {a : α} {l : List α} :

lake-manifest.json

@@ -1,9 +1,11 @@
-{"version": 4,
+{"version": 5,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
  {"url": "https://github.com/leanprover/std4",
  "subDir?": null,
- "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8",
+ "rev": "49353fa54abdac7221fe27f7b57a6ed9ff559d5c",
+ "opts": {},
  "name": "std",
- "inputRev?": "main"}}]}
+ "inputRev?": "main",
+ "inherited": false}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-29
+leanprover/lean4:nightly-2023-08-17