chore: bump to v4.2.0-rc2 (#284)

* chore: adapt to leanprover/lean4#2621 * bump to v4.2.0-rc2
leanprover-community · Oct 16, 2023 · 85a0d48 · 85a0d48
1 parent 45a5325
commit 85a0d48
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git a/Std/Tactic/SimpTrace.lean b/Std/Tactic/SimpTrace.lean
@@ -48,10 +48,12 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName => -- global definitions in the environment
+    | .decl declName inv => -- global definitions in the environment
       if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← `(Parser.Tactic.simpLemma|
-          $(mkIdent (← unresolveNameGlobal declName)):ident))
+        args := args.push (← if inv then
+          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
+        else
+          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
     | .fvar fvarId => -- local hypotheses in the context
       if let some ldecl := lctx.find? fvarId then
         localsOrStar := localsOrStar.bind fun locals =>

diff --git a/Std/Tactic/Simpa.lean b/Std/Tactic/Simpa.lean
@@ -71,10 +71,12 @@ private def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax.Tac
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName => -- global definitions in the environment
+    | .decl declName inv => -- global definitions in the environment
       if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push
-          (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
+        args := args.push (← if inv then
+          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
+        else
+          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
     | .fvar fvarId => -- local hypotheses in the context
       if isSimpAll then
         continue

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc1
+leanprover/lean4:v4.2.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.2.0-rc1
		leanprover/lean4:v4.2.0-rc2