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

Support Fact for the slim_check tactic #12565

Closed
grhkm21 opened this issue May 1, 2024 · 0 comments
Closed

Support Fact for the slim_check tactic #12565

grhkm21 opened this issue May 1, 2024 · 0 comments

Comments

@grhkm21
Copy link
Collaborator

grhkm21 commented May 1, 2024 •
edited

Currently, this fails:

import Mathlib.Tactic.SlimCheck

example {a : ℕ} [Fact a.Prime] : a + 1 = 1 + a := by
  slim_check

While replacing the [Fact a.Prime] instance with (ha : a.Prime) makes it work (with a warning of "Gave up 3 times"). It would be nice for slim_check to support Fact too!
@grhkm21 grhkm21 changed the title Support ` Support Fact for the slim_check tactic May 1, 2024
kmill added a commit that referenced this issue May 1, 2024
@kmill
feat: make Fact testable for slim_check
0df1d78 
Closes #12565
@kmill kmill mentioned this issue May 1, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue May 1, 2024
@kmill
feat: make Fact testable for slim_check (#12566)
d62ca19 
Closes #12565

Also adds a sort-of-missing `g.withContext`. I don't think its absence causes any errors.
@mathlib-bors mathlib-bors bot closed this as completed in 59710fc May 1, 2024
apnelson1 pushed a commit that referenced this issue May 12, 2024
@kmill @apnelson1
feat: make Fact testable for slim_check (#12566)
8bff94a 
Closes #12565

Also adds a sort-of-missing `g.withContext`. I don't think its absence causes any errors.
callesonne pushed a commit that referenced this issue May 16, 2024
@kmill @callesonne
feat: make Fact testable for slim_check (#12566)
0dae4cd 
Closes #12565

Also adds a sort-of-missing `g.withContext`. I don't think its absence causes any errors.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Merged by Bors] - feat: make Fact testable for slim_check leanprover-community/mathlib4
1 participant
@grhkm21