kdrag.modal.PImplies

kdrag.modal.PImplies(p: PBoolRef, q: PBoolRef, prefix='t') → PBoolRef

Pointwise Implies

>>> t = smt.Const("t", smt.IntSort())
>>> PImplies(smt.Lambda([t], t > 0), smt.Lambda([t], t > 1))
Lambda(t!..., Implies(t!... > 0, t!... > 1))

Parameters:

• p (PBoolRef)

• q (PBoolRef)

Return type:

PBoolRef