Def Lean.MVarId.rfl

Modification history

2023-10-19 08:30
Mathlib/Tactic/Relation/Rfl.lean
chore: bump dependencies (#7767)
Deleted Lean.MVarId.rflView on Github →
2023-05-03 14:00
Mathlib/Tactic/Relation/Rfl.lean
refactor, fix: `MetaM` version of `rfl` tactic and missing `whnfR`/`instantiateMVars` (#3758) …
Added Lean.MVarId.rflView on Github →