Commit 2021-09-29 17:02 82407e45

View on Github →

feat(Tactic/SolveByElim): minimal implementation (#43) This is far from feature-parity with mathlib3's SolveByElim, but has the basic functionality. I'll add more later.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Lean/LocalContext.lean

added def Lean.LocalContext.firstDeclM

added def Lean.LocalContext.lastDeclM

Created Mathlib/Tactic/SolveByElim.lean

added def Lean.Meta.solveByElim

Created Mathlib/Test/SolveByElim.lean

added def test1

added def test2

added def test3

added def test4

added def test5

added def test6