Skip to content

add new pow_to_pexpr rule#1

Open
holtzermann17 wants to merge 1 commit intorobertylewis:masterfrom
holtzermann17:pow_to_pexpr
Open

add new pow_to_pexpr rule#1
holtzermann17 wants to merge 1 commit intorobertylewis:masterfrom
holtzermann17:pow_to_pexpr

Conversation

@holtzermann17
Copy link

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant