Commit 2026-03-05 09:00 45362d78
View on Github →feat: add dsimp% elaborator (#36043)
This PR adds a dsimp% elaborators that puts a given term in dsimp-normal form. This is useful as a way to avoid the
have foo := …; dsimp at foo; rw [foo] pattern.
From SymmMonCoherence