From 12f1774374faa708b65cd7edff75db7acce4cf84 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Wed, 10 Dec 2025 19:51:56 -0800 Subject: [PATCH] chore: backtick identifiers in Ext/Simpa messages --- src/Lean/Elab/Tactic/Ext.lean | 4 ++-- src/Lean/Elab/Tactic/Simpa.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index 3392fb74af4f..2106991c5e24 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/src/Lean/Elab/Tactic/Ext.lean @@ -135,9 +135,9 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl return extName /-- -Given an 'ext' theorem, ensures that there is an iff version of the theorem (if possible), +Given an `ext` theorem, ensures that there is an iff version of the theorem (if possible), without validating any pre-existing theorems. -Returns the name of the 'ext_iff' theorem. +Returns the name of the `ext_iff` theorem. -/ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do let extIffName : Name := diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index 81d08abf39eb..5ced1d9c2c3a 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -45,7 +45,7 @@ def getLinterUnnecessarySimpa (o : LinterOptions) : Bool := let mkInfo ← mkInitialTacticInfo (mkNullNode #[tk, usingTk?.getD .missing]) let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs) (simplifyTarget := true) (discharge? := discharge?) | if getLinterUnnecessarySimpa (← getLinterOptions) then - logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'" + logLint linter.unnecessarySimpa (← getRef) "try `simp` instead of `simpa`" return {} -- Replace the goal; captured by `mkInfo` in `using` case below. replaceMainGoal [g]