Commit 2022-11-01 20:56 f8f7fd59

View on Github →

feat: upgrade solve_by_elim (#474) This is still far from feature parity with mathlib3, but at least you can add custom expressions, and omit the local context.

Estimated changes

Modified Mathlib/Tactic/LibrarySearch.lean

added def Tactic.LibrarySearch.solveByElim

Modified Mathlib/Tactic/SolveByElim.lean

added def Lean.Meta.getLocalHyps

modified def Lean.Meta.solveByElim

added def Lean.Tactic.solveByElimImpl

Modified test/SolveByElim.lean

deleted def test1

deleted def test2

deleted def test3

deleted def test4

deleted def test5

deleted def test6