Merge pull request #100 from leanprover-community/bump220126

chore: bump to nightly-2022-01-26
leanprover-community · Jan 27, 2022 · 18731e4 · 18731e4
2 parents 27c0901 + c1076d4
commit 18731e4
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/Mathport/Syntax/Translate/Tactic/Mathlib/Misc2.lean b/Mathport/Syntax/Translate/Tactic/Mathlib/Misc2.lean
@@ -192,9 +192,10 @@ attribute [trNITactic try_refl_tac] trControlLawsTac
 
 -- # order.filter.basic
 @[trTactic filter_upwards] def trFilterUpwards : TacM Syntax := do
-  `(tactic| filter_upwards
-    [$(← liftM $ (← parse pExprList).mapM trExpr),*]
-    $[$(← liftM $ (← parse (pExpr)?).mapM trExpr)]?)
+  let s ← (← parse pExprList).mapM (trExpr ·)
+  let wth := trWithIdentList (← parse withIdentList)
+  let tgt ← (← parse (tk "using" *> pExpr)?).mapM (trExpr ·)
+  `(tactic| filter_upwards [$s:term,*] $[with $[$wth:term]*]? $[using $tgt:term]?)
 
 -- # order.liminf_limsup
 @[trNITactic isBounded_default] def trIsBounded_default (_ : AST3.Expr) : M Syntax := do

diff --git a/lakefile.lean b/lakefile.lean
@@ -9,7 +9,7 @@ package mathport {
     -- as changes to tactics in mathlib4 may cause breakages here.
     -- Please ensure that `lean-toolchain` points to the same release of Lean 4
     -- as this commit of mathlib4 uses.
-    src := Source.git "https://github.com/leanprover-community/mathlib4.git" "52a7561299a5a9f7e3ba793a76321d6d40f21aee"
+    src := Source.git "https://github.com/leanprover-community/mathlib4.git" "23d4e91230a6ffa4ea1258c4b1b4a142bcdcd7c0"
   }],
   binRoot := `MathportApp
   moreLinkArgs := if Platform.isWindows then #[] else #["-rdynamic"]

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-01-23
+leanprover/lean4:nightly-2022-01-27
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2022-01-23
		leanprover/lean4:nightly-2022-01-27