Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-16 07:08
bf539287
View on Github →
chore: remove duplicate definition of MVarId.inferInstance (
#1582
)
Estimated changes
Modified
Mathlib/Lean/Meta.lean
deleted
def
Lean.MVarId.synthInstance
Modified
Mathlib/Tactic/SolveByElim.lean