We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 47423df commit 69497e4Copy full SHA for 69497e4
src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -227,7 +227,7 @@ where
227
let isRflOld ← withOptions (experimental.tactic.simp.useRflAttr.set · false) do
228
isRflProof thm.proof
229
if isRflOld then
230
- logWarning "theorem {thm.proof} is no longer rfl"
+ logWarning m!"theorem {thm.proof} is no longer rfl"
231
continue
232
if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
233
trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
0 commit comments