Skip to content

Commit d04ebac

Browse files
committed
fixes for nightly-2025-03-28
1 parent 84be192 commit d04ebac

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Diff for: Batteries/Tactic/Lint/Simp.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20for
110110
unless ← isSimpTheorem declName do return none
111111
let ctx ← Simp.Context.mkDefault
112112
checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do
113-
let isRfl := (← isRflTheorem declName).get
113+
let isRfl ← isRflTheorem declName
114114
let ({ expr := lhs', proof? := prf1, .. }, prf1Stats) ←
115115
decorateError "simplify fails on left-hand side:" <|
116116
if !isRfl then

0 commit comments

Comments
 (0)