Def Mathlib.Tactic.dsimpPercentElaborator

Modification history

2026-03-05 09:00
Mathlib/Tactic/DSimpPercent.lean
feat: add `dsimp%` elaborator (#36043) …
Added Mathlib.Tactic.dsimpPercentElaboratorView on Github →