Def Tactic.TryThis.addSuggestion

Modification history

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