Skip to content

Conversation

@leodemoura
Copy link
Member

This PR implements lia, linarith, and ac actions for grind interactive mode.

@leodemoura leodemoura requested a review from kim-em as a code owner October 17, 2025 03:47
@leodemoura leodemoura added the changelog-tactics User facing tactics label Oct 17, 2025
@leodemoura leodemoura enabled auto-merge October 17, 2025 03:47
@leodemoura leodemoura added this pull request to the merge queue Oct 17, 2025
Merged via the queue into master with commit 4ce7ad1 Oct 17, 2025
13 of 14 checks passed
Kha pushed a commit to Kha/lean4 that referenced this pull request Oct 17, 2025
This PR implements `lia`, `linarith`, and `ac` actions for `grind`
interactive mode.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants