Commit 2026-03-06 00:15 e51b9f12

View on Github →

feat(Tactic/Widget/Conv): expose API for creating conv syntax (#36157) This PR exposes some functions used by the conv? widget. This is needed for #infoview_search.

Estimated changes

Modified Mathlib/Tactic/Widget/Conv.lean

deleted inductive Mathlib.Tactic.Conv.Path

deleted def Mathlib.Tactic.Conv.pathToStx