Def Lean.MVarId.synthInstance

Modification history

2024-01-05 01:23
Mathlib/Lean/Meta.lean
chore: bump std4 dependency (#9426) …
Deleted Lean.MVarId.synthInstanceView on Github →
2023-04-18 12:01
Mathlib/Lean/Meta.lean
feat: `propose`, a forwards-reasoning analogue of `library_search`. (#2898) …
Added Lean.MVarId.synthInstanceView on Github →
2023-01-16 07:08
Mathlib/Lean/Meta.lean
chore: remove duplicate definition of MVarId.inferInstance (#1582)
Deleted Lean.MVarId.synthInstanceView on Github →
2023-01-09 15:05
Mathlib/Lean/Meta.lean
feat: refactor of solve_by_elim (#856) …
Added Lean.MVarId.synthInstanceView on Github →