def Std.Tactic.BVDecide.LRAT.Internal.State.checkEmpty (s : State) (rupHints : Array Nat) : Bool

Equations

• s.checkEmpty rupHints = s.checkRup Std.Sat.CNF.Clause.empty rupHints

theorem Std.Tactic.BVDecide.LRAT.Internal.State.entails_clause_empty_of_checkEmpty {s : State} {rupHints : Array Nat} (h : s.checkEmpty rupHints = true) : s.toCNF.EntailsClause Sat.CNF.Clause.empty