Def Lean.MVarId.postCongr!
Modification history
2023-07-14 08:37
Mathlib/Tactic/Congr!.lean
fix: control flow errors in `congr!`, and add closePre and closePost for feature parity with `congr` (#5832) …
Modified Lean.MVarId.postCongr!View on Github →