Def Mathlib.Tactic.InteractiveUnfold.InteractiveUnfold.rpc

Modification history

2026-06-11 22:17

Mathlib/Tactic/ClickSuggestions/Unfold.lean

feat(Tactic): `#click_suggestions` (#39433) …

Deleted Mathlib.Tactic.InteractiveUnfold.InteractiveUnfold.rpc View on Github →

2026-02-07 13:29

Mathlib/Tactic/Widget/InteractiveUnfold.lean

fix(unfold?): make the RPC function public (#34925) …

Added Mathlib.Tactic.InteractiveUnfold.InteractiveUnfold.rpc View on Github →