-
Notifications
You must be signed in to change notification settings - Fork 251
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.
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
[Merged by Bors] - refactor: List.All₂ to List.Forall #7797
Conversation
This renames `List.All₂` to `List.Forall`, because the `₂` is highly confusing when it usually means “two lists”, and we had users on Zulip not find `List.Forall` because of that (<https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Is.20there.20List.2EForall.E2.82.82.2C.20but.20for.20one.20list.3F.20.28In.20library.20Std.29/near/397551365>) This also * Switches to primitive recursion, so that `all₂_cons` holds definitially and can be dropped * Updates all affected proofs * In `NumberTheory/Dioph`, a non-terminal `simp at d` could be removed completely because of this defeq. * I also `simp-only`ied another non-terminal `simp` there.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ nomeata can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
This renames `List.All₂` to `List.Forall`, because the `₂` is highly confusing when it usually means “two lists”, and we had users on Zulip not find `List.Forall` because of that (<https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Is.20there.20List.2EForall.E2.82.82.2C.20but.20for.20one.20list.3F.20.28In.20library.20Std.29/near/397551365>)
Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause |
Canceled. |
bors merge |
This renames `List.All₂` to `List.Forall`, because the `₂` is highly confusing when it usually means “two lists”, and we had users on Zulip not find `List.Forall` because of that (<https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Is.20there.20List.2EForall.E2.82.82.2C.20but.20for.20one.20list.3F.20.28In.20library.20Std.29/near/397551365>) Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This renames `List.All₂` to `List.Forall`, because the `₂` is highly confusing when it usually means “two lists”, and we had users on Zulip not find `List.Forall` because of that (<https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Is.20there.20List.2EForall.E2.82.82.2C.20but.20for.20one.20list.3F.20.28In.20library.20Std.29/near/397551365>) Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This renames
List.All₂
toList.Forall
, because the₂
is highlyconfusing when it usually means “two lists”, and we had users on Zulip
not find
List.Forall
because of that(https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Is.20there.20List.2EForall.E2.82.82.2C.20but.20for.20one.20list.3F.20.28In.20library.20Std.29/near/397551365)