kdrag.kernel.make_unfolding
- kdrag.kernel.make_unfolding(pf: Proof) Unfolding
Take an axiom of the form |= forall x0 x1 …, xn, f(x0, x1, …, xn) = body and return a Defn object for f. Unfolding judgments can be used with unfold_defns.
>>> x,y,z = smt.Ints("x y z") >>> pf = kd.prove(smt.ForAll([x,y], x + y == y + x + 0)) # has shape of definition, but not "definitional" >>> defn = make_unfolding(pf) >>> unfold_defns(z + 42, [defn]) (42 + z + 0, |= z + 42 == 42 + z + 0)