kdrag.kernel.substitute_schema_vars

kdrag.kernel.substitute_schema_vars(pf: Proof, *subst) → Proof

Substitute schematic variables in a theorem. This is is single step instead of generalizing to a Forall and then eliminating it.

>>> x = SchemaVar("x", smt.IntSort())
>>> y = SchemaVar("y", smt.IntSort())
>>> substitute_schema_vars(prove(x == x), (x, smt.IntVal(42)), (y, smt.IntVal(43)))
|- 42 == 42

Parameters:

pf (Proof)

Return type:

Proof