Inductive Mathlib.Tactic.Conv.Path

Modification history

2026-03-06 00:15
Mathlib/Tactic/Widget/Conv.lean
feat(Tactic/Widget/Conv): expose API for creating conv syntax (#36157) …
Deleted Mathlib.Tactic.Conv.PathView on Github →
2026-01-13 15:36
Mathlib/Tactic/Widget/Conv.lean
fix(Tactic/Widget/Conv): fix various issues (#25889) …
Added Mathlib.Tactic.Conv.PathView on Github →