Add xor to LEAN #520
Add xor to LEAN #520
Conversation
src/form/lean.cpp
Outdated
| if (expr.name == "bitxor") { | ||
| if (expr.children.size() != 2) return false; | ||
| Expression f(Expression::Type::FUNCTION, "Int.xor", {expr.children[0], expr.children[1]}); | ||
| expr = f; |
|
|
||
| std::string LeanFormula::printEvalCode(int64_t offset, int64_t numTerms) const { | ||
| std::stringstream out; | ||
| out << "import Mathlib.Data.Int.Bitwise" << std::endl; |
There was a problem hiding this comment.
Install it in the GH workflow
| A008531: def a (n : Int) : Int := (Bool.toInt (n==0))+n*(5*n^2+5) | ||
| A021019: def a (n : Int) : Int := 6*(min n 1) | ||
| A060576: def a (n : Int) : Int := Bool.toInt (n != 1) | ||
| A092242: def a (n : Int) : Int := 2*(Int.xor (3*n-3) 1)+3 |
There was a problem hiding this comment.
Could you add more examples?
|
You can use Copilot to fix GH workflow issue |
There was a problem hiding this comment.
Pull Request Overview
This PR adds support for the bitwise XOR operation in the LEAN formula conversion system. The purpose is to enable LODA to generate LEAN code that includes XOR operations when converting mathematical expressions to LEAN syntax.
- Adds handling for "bitxor" expressions in the LEAN converter to output "Int.xor"
- Includes necessary import statement for bitwise operations in LEAN
- Adds test case for sequence A092242 which uses XOR operations
Reviewed Changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| src/form/lean.cpp | Implements bitxor to Int.xor conversion and adds required import |
| tests/formula/lean.txt | Adds test case for A092242 sequence using XOR operation |
| if (expr.name == "bitxor") { | ||
| if (expr.children.size() != 2) return false; | ||
| Expression f(Expression::Type::FUNCTION, "Int.xor", {expr.children[0], expr.children[1]}); | ||
| expr = f; | ||
| break; | ||
| } |
There was a problem hiding this comment.
[nitpick] The bitxor handling code duplicates the pattern used for min/max operations. Consider extracting the common binary function conversion logic to reduce code duplication.
|
Replaced by #522 |
2 participants
No description provided.