kdrag.notation.QImplies

kdrag.notation.QImplies(*hyp_conc) → BoolRef

Quantified Implies

Shorthand for Implies(And(hyp[0], hyp[1], …), conc)

>>> x,y = smt.Ints("x y")
>>> QImplies(x > 0, y > 0, x + y > 0)
Implies(And(x > 0, y > 0), x + y > 0)