kdrag.kernel.eqrefl

kdrag.kernel.eqrefl(x: ExprRef) → Proof

Prove reflexivity of equality

>>> x = smt.Int("x")
>>> eqrefl(x)
|- x == x

Parameters:

x (ExprRef)

Return type:

Proof