chore: allow omega to use classicality, in case Decidable instances are too big

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed semorrison closed 1 week ago

semorrison commented 1 week ago

leanprover-community-mathlib4-bot commented 1 week ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3bd2a7419df83fd9bdec8c480b52cc1ff340933e --onto 00cf5771f31e7de7f6ab3089cb4b9ffa606a35ed. (2024-05-06 04:53:43)
❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3bd2a7419df83fd9bdec8c480b52cc1ff340933e --onto e362b50fa95d6823e59dd706803a93c25e888535. (2024-05-06 11:30:04)