Def Tactic.TryThis.addTermSuggestion

Modification history

2022-09-27 16:29
Mathlib/Tactic/TryThis.lean
chore: update lean + std4 09-26 (#443)
Deleted Tactic.TryThis.addTermSuggestionView on Github →
2021-10-14 07:32
Mathlib/Tactic/TryThis.lean
feat(Tactic/ShowTerm): port of show_term (#44) …
Added Tactic.TryThis.addTermSuggestionView on Github →