kdrag.theories.univ.poly_ax

kdrag.theories.univ.poly_ax(s: SortRef) → Proof
>>> kd.prove(cast(smt.IntSort(), box(smt.IntVal(42))) == 42, by=[poly_ax(smt.IntSort())])
|= cast_Int(box(42)) == 42
Parameters:

s (SortRef)

Return type:

Proof