chore: forward port leanprover-community/mathlib#19228 (#5843)

The implementation in Mathlib 4 doesn't use `mapAccumLM` so the thing to do is only updating the header.
leanprover-community · Jul 13, 2023 · 5cdfdb8 · 5cdfdb8
1 parent b41e763
commit 5cdfdb8
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 
 ! This file was ported from Lean 3 source module control.traversable.derive
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit b01d6eb9d0a308807af54319b264d0994b91774b
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

diff --git a/test/Traversable.lean b/test/Traversable.lean
@@ -51,6 +51,13 @@ inductive MyTree (α : Type)
 
 #guard_msgs (drop info) in #synth LawfulTraversable MyTree
 
+inductive MyTree' (α : Type)
+  | leaf : MyTree' α
+  | node : MyTree' α → α → MyTree' α → MyTree' α
+  deriving LawfulTraversable
+
+#guard_msgs (drop info) in #synth LawfulTraversable MyTree'
+
 section
 open MyTree hiding traverse