Commit 2024-06-04 00:39 9f8031e0

View on Github →

fix(Tactic/Elementwise): type inference in elementwise (#13413) added an optional type argument to SimpType; changed type inference in elementwise tactic

Estimated changes

Modified Mathlib/Lean/Meta/Simp.lean

modified def Lean.Meta.Simp.simpType

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

Modified test/CategoryTheory/Elementwise.lean

added def ElementwiseTest.f

added theorem ElementwiseTest.fh

added def ElementwiseTest.g

added theorem ElementwiseTest.gh

added def ElementwiseTest.h