kdrag.kernel.subst

kdrag.kernel.subst(t: ExprRef, eqs: Sequence[Proof]) → tuple[ExprRef, Proof]

Substitute using equality proofs

>>> x, y = smt.Ints("x y")
>>> eq = kd.prove(x == ((x + 1) - 1))
>>> subst(x + 3, [eq])
(x + 1 - 1 + 3, |= x + 3 == x + 1 - 1 + 3)

Parameters:

• t (ExprRef)

• eqs (Sequence[Proof])

Return type:

tuple[ExprRef, Proof]