Lean4
@[inherit_doc Mathlib.Linter.linter.style.show]
def showLinter : Linter where
run :=
withSetOptionIn fun stx => do
unless getLinterValue linter.style.show (← getLinterOptions) do
return
if (← get).messages.hasErrors then
return
for tree in (← getInfoTrees)do
tree.foldInfoM (init := ()) fun ci i _ => do
let .ofTacticInfo tac := i |
return
unless tac.stx.isOfKind ``Lean.Parser.Tactic.show do
return
let some _ := tac.stx.getRange? true |
return
let (goal :: goals) := tac.goalsBefore |
return
let (goal' :: goals') := tac.goalsAfter |
return
if goals != goals' then
return -- `show` didn't act on first goal -> can't replace with `change`
if goal == goal' then
return -- same goal, no need to check
let diff ←
ci.runCoreM
(do
let before ←
(do
instantiateMVars (← goal.getType)).run'
{ } { mctx := tac.mctxBefore }
let after ←
(do
instantiateMVars (← goal'.getType)).run'
{ } { mctx := tac.mctxAfter }
return before != after)
if diff then
logLint linter.style.show tac.stx
m!"\
The `show` tactic should only be used to indicate intermediate goal states for \
readability.\nHowever, this tactic invocation changed the goal. Please use `change` \
instead for these purposes."
