preprocess — Mathlib

Lean4
/-- `preprocess pps l` takes a list `l` of proofs of propositions.
It maps each preprocessor `pp ∈ pps` over this list.
The preprocessors are run sequentially: each receives the output of the previous one.
Note that a preprocessor may produce multiple or no expressions from each input expression,
so the size of the list may change.
-/
def preprocess (pps : List GlobalBranchingPreprocessor) (g : MVarId) (l : List Expr) : MetaM (List Branch) := do
  withTraceNode `linarith (fun e => return m! "{exceptEmoji e} Running preprocessors") <|
      g.withContext <|
        pps.foldlM (init := [(g, l)]) fun ls pp => do
          return
            (←
                ls.mapM fun (g, l) => do
                  pp.process g l).flatten
Похожие утверждения