Def Mathlib.Tactic.Push.elabHead

Modification history

2025-09-23 03:07

Mathlib/Tactic/Push.lean

feat: extensible `push` and `pull` tactics (#21965) …

Added Mathlib.Tactic.Push.elabHead View on Github →