mergeWithGrind — Mathlib

Lean4
@[tacticAnalysis linter.tacticAnalysis.mergeWithGrind, inherit_doc linter.tacticAnalysis.mergeWithGrind]
def mergeWithGrind : TacticAnalysis.Config where
  run
    seq := do
    if let #[(preCtx, preI), (_postCtx, postI)] := seq[0:2].array then
      if postI.stx.getKind == ``Lean.Parser.Tactic.grind then
        if let [goal] := preI.goalsBefore then
          let goals ←
            try
              preCtx.runTacticCode preI goal postI.stx
            catch _e =>
              pure [goal]
          if goals.isEmpty then
            logWarningAt preI.stx m! "'{preI.stx}; grind' can be replaced with 'grind'"
Похожие утверждения