mathematica icon indicating copy to clipboard operation
mathematica copied to clipboard

add new pow_to_pexpr rule

Open holtzermann17 opened this issue 5 years ago • 0 comments

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

holtzermann17 avatar Mar 29 '19 12:03 holtzermann17