kdrag.modal.PDistinct

kdrag.modal.PDistinct(*args, prefix='t') → PBoolRef

Pointwise Distinct

>>> t = smt.Const("t", smt.IntSort())
>>> PDistinct(smt.Lambda([t], t), smt.Lambda([t], t + 1))
Lambda(t!..., t!...  != t!... + 1)