runPasses — Mathlib

Lean4
/-- Run the tactic analysis passes from `configs` on the tactic sequences in `stx`,
using `trees` to get the infotrees. -/
def runPasses (configs : Array Pass) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM Unit := do
  let opts ← getLinterOptions
  let enabledConfigs :=
    configs.filter
      fun config =>
        -- This can be `none` in the file where the option is declared.

      if let some opt := config.opt then getLinterValue opt opts else false
  if enabledConfigs.isEmpty then
    return
  for i in trees do
    for seq in (← findTacticSeqs stx i)do
      for config in enabledConfigs do
        config.run seq
Похожие утверждения