Skip to content

Conversation

@leodemoura
Copy link
Member

This PR adds the mbtc tactic to the grind interactive mode. It implements model-based theory combination. It also ensures finish? is capable of generating it.

This PR adds the `mbtc` tactic to the `grind` interactive mode. It
implements model-based theory combination. It also ensures `finish?`
is capable of generating it.
@leodemoura leodemoura added the changelog-tactics User facing tactics label Oct 25, 2025
@leodemoura leodemoura requested a review from kim-em as a code owner October 25, 2025 03:22
@leodemoura leodemoura enabled auto-merge October 25, 2025 03:22
@leodemoura leodemoura added this pull request to the merge queue Oct 25, 2025
Merged via the queue into master with commit 3c2ab0f Oct 25, 2025
14 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
)

This PR adds the `mbtc` tactic to the `grind` interactive mode. It
implements model-based theory combination. It also ensures `finish?` is
capable of generating it.
kim-em pushed a commit that referenced this pull request Oct 27, 2025
This PR adds the `mbtc` tactic to the `grind` interactive mode. It
implements model-based theory combination. It also ensures `finish?` is
capable of generating it.
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