Skip to content

Commit

Permalink
feat: upstream 'Try this:' widgets (#3266)
Browse files Browse the repository at this point in the history
There is a test file in Std that should later be reunited with this
code.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
  • Loading branch information
kim-em and Kha authored Feb 13, 2024
1 parent 644d426 commit fdc64de
Show file tree
Hide file tree
Showing 3 changed files with 630 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/Lean/Meta/Tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ import Lean.Meta.Tactic.Simp
import Lean.Meta.Tactic.AuxLemma
import Lean.Meta.Tactic.SplitIf
import Lean.Meta.Tactic.Split
import Lean.Meta.Tactic.TryThis
import Lean.Meta.Tactic.Cleanup
import Lean.Meta.Tactic.Unfold
import Lean.Meta.Tactic.Rename
Expand Down
Loading

0 comments on commit fdc64de

Please sign in to comment.