chore: update lean

leanprover-community · Jul 31, 2023 · 03139ed · 03139ed
1 parent 52223db
commit 03139ed
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean b/Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean
@@ -29,7 +29,8 @@ open Parser
   `(tactic| init_ring $[using $(← liftM $ (← parse (tk "using" *> pExpr)?).mapM trExpr)]?)
 
 @[tr_tactic ghost_simp] def trGhostSimp : TacM Syntax.Tactic := do
-  `(tactic| ghost_simp $[[$((← trSimpArgs (← parse simpArgList)).asNonempty),*]]?)
+  let args := (← trSimpArgs (← parse simpArgList)).asNonempty
+  `(tactic| ghost_simp $[[$args,*]]?)
 
 @[tr_tactic witt_truncate_fun_tac] def trWittTruncateFunTac : TacM Syntax.Tactic :=
   `(tactic| witt_truncate_fun_tac)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -16,7 +16,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "f39466cb99f0b941b72e1d918d139ef25a419023",
+    "rev": "dc89373908a65cd4807c248c566cbb75c18328f9",
     "name": "mathlib",
     "inputRev?": "master"}},
   {"git":

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-24
+leanprover/lean4:nightly-2023-07-30
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2023-07-24
		leanprover/lean4:nightly-2023-07-30