Def addRefineSuggestion

Modification history

2023-05-17 12:05
Mathlib/Tactic/TryThis.lean
chore: bump dependencies (#4012) …
Deleted addRefineSuggestionView on Github →
2023-05-02 22:58
Mathlib/Tactic/TryThis.lean
feat: better display of partial results from library_search (#3743) …
Added addRefineSuggestionView on Github →