checkAndSortRewriteLemmas — Mathlib

Lean4
/-- Try to rewrite `e` with each of the rewrite lemmas, and sort the resulting rewrites. -/
def checkAndSortRewriteLemmas (e : Expr) (rewrites : Array RewriteLemma) : MetaM (Array (Rewrite × Name)) := do
  let rewrites ←
    rewrites.filterMapM fun rw =>
        tryCatchRuntimeEx
          (do
            let thm ← mkConstWithFreshMVarLevels rw.name
            Option.map (·, rw.name) <$> checkRewrite thm e rw.symm)
          fun _ => return none
  let lt (a b : (Rewrite × Name)) :=
    Ordering.isLT <|
      (compare a.1.extraGoals.size b.1.extraGoals.size).then <|
        (compare a.1.symm b.1.symm).then <|
          (compare a.2.toString.length b.2.toString.length).then <|
            (compare a.1.stringLength b.1.stringLength).then <| (Name.cmp a.2 b.2)
  return rewrites.qsort lt
Похожие утверждения