Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: add lemma code-action #625

Merged
merged 10 commits into from
Aug 16, 2024
Prev Previous commit
Next Next commit
Merge branch 'main' into adomani/lemma_vs_theorem
  • Loading branch information
adomani authored Apr 23, 2024
commit 8591d4c39dcd31fe70a8b4206f6c0c5863950968
4 changes: 0 additions & 4 deletions Std.lean
Original file line number Diff line number Diff line change
@@ -81,10 +81,6 @@ import Std.Tactic.Congr
import Std.Tactic.Exact
import Std.Tactic.Init
import Std.Tactic.Instances
import Std.Tactic.LabelAttr
import Std.Tactic.LeftRight
import Std.Tactic.Lemma
import Std.Tactic.LibrarySearch
import Std.Tactic.Lint
import Std.Tactic.Lint.Basic
import Std.Tactic.Lint.Frontend
2 changes: 0 additions & 2 deletions Std/Tactic/Basic.lean
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
import Lean.Elab.Tactic.ElabTerm
import Std.Linter
import Std.Tactic.Init
import Std.Tactic.Lemma
import Std.Tactic.NoMatch
import Std.Tactic.SeqFocus
import Std.Util.ProofWanted

Loading
You are viewing a condensed version of this merge commit. You can view the full changes here.