Def addHaveSuggestion

Modification history

2024-01-30 01:07
Mathlib/Tactic/TryThis.lean
chore: bump Std to leanprover/std4#242 (#10104)
Deleted addHaveSuggestionView on Github →
2024-01-08 13:15
Mathlib/Tactic/TryThis.lean
feat: allow naming the hypothesis generated by have? (#9454) …
Modified addHaveSuggestionView on Github →
2023-07-27 17:38
Mathlib/Tactic/TryThis.lean
feat: replace have? correctly (#5305) …
Modified addHaveSuggestionView on Github →
2023-05-17 12:05
Mathlib/Tactic/TryThis.lean
chore: bump dependencies (#4012) …
Modified addHaveSuggestionView on Github →
2023-04-20 08:29
Mathlib/Tactic/TryThis.lean
feat: port observe tactic from mathlib (#3516)
Modified addHaveSuggestionView on Github →
2023-04-18 12:01
Mathlib/Tactic/TryThis.lean
feat: `propose`, a forwards-reasoning analogue of `library_search`. (#2898) …
Added addHaveSuggestionView on Github →