kdrag.tactics.PTheorem

kdrag.tactics.PTheorem(goal: BoolRef | str)

A decorator to create a theorem from a function that takes a ProofState as argument.

>>> x = smt.Int("x")
>>> @PTheorem(x + 1 > x)
... def mytheorem(l: ProofState):
...     "An example theorem"
...     l.auto()
Lemma Complete! Change PTheorem to Theorem

Parameters:

goal (BoolRef | str)