kdrag.tactics.vprove

kdrag.tactics.vprove(thm: BoolRef, **kwargs) → Proof

Prove a theorem using an egraph-based solver.

>>> x = smt.Int("x")
>>> vprove(x + 1 > x)
|= x + 1 > x