kdrag.property.LeftIdentity

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

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

Parameters:

e (ExprRef)

Return type:

BoolRef