Def Mathlib.Tactic.ClickSuggestions.addSolvingSuggestion

Modification history

2026-10-17 01:01

Mathlib/Tactic/ClickSuggestions/Util.lean

feat(ClickSuggestions): use the tactic as the button text (#44894) …

Added Mathlib.Tactic.ClickSuggestions.addSolvingSuggestion View on Github →