Commit 2026-02-07 13:29 e2df8d44

View on Github →

fix(unfold?): make the RPC function public (#34925) This PR applies the fix of #34474 to unfold?

Estimated changes

Modified Mathlib/Tactic/Widget/InteractiveUnfold.lean

added def Mathlib.Tactic.InteractiveUnfold.InteractiveUnfold.rpc