Def Lean.MVarId.note

Modification history

2024-01-05 01:23
Mathlib/Lean/Meta.lean
chore: bump std4 dependency (#9426) …
Deleted Lean.MVarId.noteView on Github →
2023-01-09 15:05
Mathlib/Lean/Meta.lean
feat: refactor of solve_by_elim (#856) …
Modified Lean.MVarId.noteView on Github →
2022-11-07 21:25
Mathlib/Tactic/ApplyFun.lean
feat: port apply_fun (#475) …
Added Lean.MVarId.noteView on Github →