Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: equality proof generation for grind #6452

Merged
merged 6 commits into from
Dec 26, 2024
Merged

feat: equality proof generation for grind #6452

merged 6 commits into from
Dec 26, 2024

Conversation

leodemoura
Copy link
Member

This PR adds support for generating (small) proofs for any two expressions that belong to the same equivalence class in the grind tactic state.

@leodemoura leodemoura added the changelog-language Language features, tactics, and metaprograms label Dec 26, 2024
@leodemoura leodemoura enabled auto-merge December 26, 2024 05:47
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 26, 2024 05:56 Inactive
@leodemoura leodemoura added this pull request to the merge queue Dec 26, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 26, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bdcb7914b5e3f2b89498d9cdd8f923dd20633150 --onto f9f8abe2a3eb0591cef3769e2a51717fb2b9a166. (2024-12-26 06:05:50)

Merged via the queue into master with commit 8a1e50f Dec 26, 2024
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@leodemoura @leanprover-community-bot