Commit 2025-06-03 17:48 2f402e01
View on Github →chore: remove dsimp
when followed by simp
(#25391)
Now that my simp
optimizations have landed, I'm testing the hypothesis that dsimp
followed by simp
is slower than just simp
.
By the way, I can't find the [dsimp, simp] library note anywhere. Has it disappeared?