collectFacts — Mathlib

Lean4
/-- Collects facts from the local context. For each occurring type `α`, the returned map contains
a pair `(idxToAtom, facts)`, where the map `idxToAtom` converts indices to found
atomic expressions of type `α`, and `facts` contains all collected `AtomicFact`s about them. -/
def collectFacts : MetaM <| Std.HashMap Expr <| Std.HashMap Nat Expr × Array AtomicFact := do
  let res := (← collectFactsImp.run ∅).snd
  return
    res.map fun _ (atomToIdx, facts) =>
      let idxToAtom : Std.HashMap Nat Expr :=
        atomToIdx.fold (init := ∅) fun acc _ value => acc.insert value.fst value.snd
      (idxToAtom, facts)
Похожие утверждения