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: check pattern coverage in the grind_pattern command #6474

Merged
merged 2 commits into from
Dec 30, 2024
Merged

feat: check pattern coverage in the grind_pattern command #6474

merged 2 commits into from
Dec 30, 2024

Conversation

leodemoura
Copy link
Member

This PR adds pattern validation to the grind_pattern command. The new checkCoverage function will also be used to implement the attributes @[grind_eq], @[grind_fwd], and @[grind_bwd].

@leodemoura
chore: add info for grind_pattern theorem name
4e2b0f5
@leodemoura
feat: check pattern coverage in grind_pattern
1338a86 
This PR adds pattern validation to the `grind_pattern` command.
The new `checkCoverage` function will also be used to implement the attributes
`@[grind_eq]`, `@[grind_fwd]`, and `@[grind_bwd]`.
@leodemoura leodemoura added the changelog-language Language features, tactics, and metaprograms label Dec 30, 2024
@leodemoura leodemoura requested a review from kim-em as a code owner December 30, 2024 03:25
@leodemoura leodemoura enabled auto-merge December 30, 2024 03:25
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 30, 2024 03:38 Inactive
@leodemoura leodemoura added this pull request to the merge queue Dec 30, 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 30, 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 3c326d771caed3b730c3a1986a13b15f90beaf76 --onto 536c6a8ea6b298773fed5e8dce82c3faff43dac4. (2024-12-30 03:44:27)

Merged via the queue into master with commit 24a8561 Dec 30, 2024
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

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