mathematica
mathematica copied to clipboard
add new pow_to_pexpr rule
I found that I needed a pow_to_pexpr
to complete the translation of
ProveUsingLeanTactic[
ForAllTyped[{x, y}, real, Equal[Hold[Power[x + y, 2]], Hold[x ^ 2 + 2 * x * y + y ^ 2]]],
"`[mm_prover]", LeanExecutable, True]
->
"AY[ForAllTyped][AY[List][Y[x],Y[y]],Y[real],AY[Equal][AY[Hold][AY[Power][AY[Plus][Y[x],Y[y]],I[2]]],AY[Hold][AY[Plus][AY[Power][Y[x],I[2]],AY[Times][I[2],Y[x],Y[y]],AY[Power][Y[y],I[2]]]]]]"
->
∀ (x y : ℝ), (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2