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

Adapt classical to new semantics #306

Closed
gebner opened this issue Jul 18, 2022 · 0 comments
Closed

Adapt classical to new semantics #306

gebner opened this issue Jul 18, 2022 · 0 comments
Labels
good first issue Good for newcomers

Comments

@gebner
Copy link
Member

gebner commented Jul 18, 2022

We've recently changed classical in mathlib to so that it no longer overrides the existing decidable instances. mathlib4 should be adapterd. leanprover-community/mathlib#14122

import Mathlib.Tactic.Basic

example : (by classical; exact decide (0 = 1) : Bool) = decide (0 = 1) := rfl -- this should work
@gebner gebner added the good first issue Good for newcomers label Jul 18, 2022
@Komyyy Komyyy closed this as completed Jul 12, 2023
bustercopley added a commit that referenced this issue Oct 21, 2023
@bustercopley
Update dependencies for CI (do not merge)
400cc88 
For Mathlib #7812 dependency on core #2721 and std #306
* lean-toolchain: leanprover/lean4-pr-releases:pr-release-2721
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
bustercopley added a commit that referenced this issue Oct 21, 2023
@bustercopley
Update dependencies for CI (do not merge)
d8d37cc 
For Mathlib #7812 dependency on core #2721 and std #306
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
bustercopley added a commit that referenced this issue Oct 22, 2023
@bustercopley
Update dependencies for CI (do not merge)
6a3c135 
For Mathlib #7812 dependency on core #2721 and std #306
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
bustercopley pushed a commit that referenced this issue Oct 22, 2023
@leanprover-community-mathlib4-bot @bustercopley
Update dependencies for CI (do not merge)
3665052 
For Mathlib #7812 dependency on core #2721 and std #306
* lean-toolchain: leanprover/lean4-pr-releases:pr-release-2721
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
good first issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gebner @Komyyy