kdrag.rewrite.horn_of_theorem

kdrag.rewrite.horn_of_theorem(thm: ExprRef | Proof) → Rule

Unpack theorem of form forall vs, body => head into a Rule tuple

>>> x = smt.Real("x")
>>> horn_of_theorem(smt.ForAll([x], smt.Implies(x**2 == x*x, x > 0)))
Rule(vs=[X...], hyp=X...**2 == X...*X..., conc=X... > 0, pf=None)

Parameters:

thm (ExprRef | Proof)

Return type:

Rule