kdrag.modal.PEq

kdrag.modal.PEq(x: PExprRef, y: PExprRef) → PBoolRef

Pointwise equality rather than on the nose equality.

>>> x = smt.Int("x")
>>> PointEq(smt.Lambda([x], x), 1)
Lambda(x0!..., x0!... == 1)

Parameters:

• x (PExprRef)

• y (PExprRef)

Return type:

PBoolRef