kdrag.theories.logic.temporal.Implies

kdrag.theories.logic.temporal.Implies(x: DatatypeRef, y: DatatypeRef) → DatatypeRef

>>> x,y = smt.Consts("x y", TSort(smt.BoolSort()))
>>> smt.simplify(Valid(Implies(x, y)))
Or(Not(val(x)[0]), val(y)[0])

Parameters:

• x (DatatypeRef)

• y (DatatypeRef)

Return type:

DatatypeRef