kdrag.property.RightIdentity

kdrag.property.RightIdentity(f, e: ExprRef, T=None) → BoolRef

>>> RightIdentity(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()), smt.IntVal(0))
ForAll(x, f(x, 0) == x)

Parameters:

e (ExprRef)

Return type:

BoolRef