constructLeGraph — Mathlib

Lean4
/-- Constructs a directed `Graph` using `≤` facts. It also creates edges from `⊥`
(if present) to all vertices and from all vertices to `⊤` (if present). -/
def constructLeGraph (nVertexes : Nat) (facts : Array AtomicFact) (idxToAtom : Std.HashMap Nat Expr) : MetaM Graph := do
  let mut res : Graph := Array.replicate nVertexes #[]
  for fact in facts do
    if let .le lhs rhs proof := fact then
      res := res.addEdge ⟨lhs, rhs, proof⟩
    else if let .isTop idx := fact then
      for i in [:nVertexes]do
        if i != idx then
          res := res.addEdge ⟨i, idx, ← mkAppOptM ``le_top #[none, none, none, idxToAtom.get! i]⟩
    else if let .isBot idx := fact then
      for i in [:nVertexes]do
        if i != idx then
          res := res.addEdge ⟨idx, i, ← mkAppOptM ``bot_le #[none, none, none, idxToAtom.get! i]⟩
  return res
Похожие утверждения