checkEqc — Mathlib

Lean4
/-- Check for integrity of the `CCState`. -/
def checkEqc (ccs : CCState) (e : Expr) : Bool :=
  toBool <|
    Id.run <|
      OptionT.run
        (do
          let root := ccs.root e
          let mut size : Nat := 0
          let mut it := e
          repeat
            let some itN := ccs.entries[it]? |
              failure
            guard (itN.root == root)
            let mut it₂ := it
            repeat
              let it₂N := ccs.entries[it₂]?
              match it₂N.bind Entry.target with
              | some it₃ =>
                it₂ := it₃
              | none =>
                break
            guard (it₂ == root)
            it := itN.next
            size := size + 1
          until it == e
          guard (ccs.entries[root]? |>.any (·.size == size)))
Похожие утверждения