kdrag.tactics.simp_tac

kdrag.tactics.simp_tac(e: ExprRef) → Proof

Simplify an expression using simp and return the resulting equality as a proof.

>>> import kdrag.theories.nat as nat
>>> simp_tac(nat.Z + nat.S(nat.Z))
|- add(Z, S(Z)) == S(Z)

Parameters:

e (ExprRef)

Return type:

Proof