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

chore: use mixin ordered algebraic typeclasses (part 1) #20594

Open
wants to merge 101 commits into
base: master
Choose a base branch
from
Open

chore: use mixin ordered algebraic typeclasses (part 1) #20594

wants to merge 101 commits into from

Conversation

FR-vdash-bot
Copy link
Collaborator

@FR-vdash-bot FR-vdash-bot commented Jan 9, 2025 •
edited
Loading

FR-vdash-bot added 30 commits June 5, 2024 04:27
@FR-vdash-bot
Squashed commit of the following:
b1b9b64 
commit 7561e65e55f1dbba1058c43ca1701038ceed98dc
Author: negiizhao <[email protected]>
Date:   Wed Jun 5 04:26:04 2024 +0800

    fix

commit 777db8a7d19ed4d66815f9575206992ca578cb5e
Merge: cc6eede 52b851a
Author: negiizhao <[email protected]>
Date:   Wed Jun 5 04:25:36 2024 +0800

    Merge branch 'master' into FR_canonically

commit cc6eede
Author: negiizhao <[email protected]>
Date:   Thu Dec 28 15:01:00 2023 +0800

    fix

commit ae1dfda
Merge: c1931cf 1a749e0
Author: negiizhao <[email protected]>
Date:   Thu Dec 28 14:10:05 2023 +0800

    Merge branch 'FR_covariance_instance' into FR_canonically

commit c1931cf
Merge: 9e0f667 6cab3d6
Author: negiizhao <[email protected]>
Date:   Thu Dec 28 14:09:53 2023 +0800

    Merge branch 'master' into FR_canonically

commit 1a749e0
Author: negiizhao <[email protected]>
Date:   Tue Dec 26 04:24:52 2023 +0800

    revert some instance changes

commit a6e645f
Author: negiizhao <[email protected]>
Date:   Mon Dec 25 11:01:06 2023 +0800

    fix

commit 6af13a5
Author: negiizhao <[email protected]>
Date:   Mon Dec 25 10:06:19 2023 +0800

    Revert "fix"

    This reverts commit 7ebd135.

commit 63a181b
Author: negiizhao <[email protected]>
Date:   Mon Dec 25 09:49:50 2023 +0800

    hack

commit 7ebd135
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 14:25:47 2023 +0800

    fix

commit 20d2809
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 14:13:08 2023 +0800

    chore: remove redundant instances

commit 9e0f667
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 12:45:15 2023 +0800

    fix

commit bf51f25
Merge: bd9e5b4 e9fb5b3
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 12:00:56 2023 +0800

    Merge branch 'master' into FR_canonically

commit bd9e5b4
Author: negiizhao <[email protected]>
Date:   Tue Oct 24 01:49:05 2023 +0800

    nolint again

commit 6414331
Author: negiizhao <[email protected]>
Date:   Tue Oct 24 00:36:00 2023 +0800

    reduce diffs

commit 6d1f059
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 19:41:50 2023 +0800

    Revert "remove nolint"

    This reverts commit d60fc68.

commit d60fc68
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 10:24:07 2023 +0800

    remove nolint

commit 86f6ec7
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 10:23:24 2023 +0800

    fix

commit a3d8af1
Merge: 58e2ba8 801dc0d
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 09:53:43 2023 +0800

    Merge branch 'master' into FR_canonically

commit 58e2ba8
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 09:52:49 2023 +0800

    reduce diffs

commit be2b4bb
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 08:58:03 2023 +0800

    `[Mul α] [LE α]` -> `[Monoid α] [PartialOrder α]`

commit 0777b07
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 02:46:01 2023 +0800

    rerun bench please

commit 6415bc9
Author: negiizhao <[email protected]>
Date:   Sun Oct 22 18:30:20 2023 +0800

    fix

commit 14cdac7
Author: negiizhao <[email protected]>
Date:   Sun Oct 22 14:11:31 2023 +0800

    nolint

commit 5bc0815
Author: Mario Carneiro <[email protected]>
Date:   Sat Oct 21 17:30:57 2023 -0400

    chore: bump lean toolchain

commit 86c8440
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 23:50:53 2023 +0800

    fix

commit f14bdc9
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 23:07:59 2023 +0800

    fix

commit 5feb528
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 22:41:09 2023 +0800

    fix

commit 958c4a5
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 22:07:26 2023 +0800

    fix

commit fae1c85
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 21:07:44 2023 +0800

    fix

commit e6309d6
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:07:09 2023 +0800

    fix merge

commit a619670
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:06:29 2023 +0800

    oops

commit 9c3d72d
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:04:15 2023 +0800

    fix merge

commit 8a76d2e
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:01:16 2023 +0800

    fix merge

commit 7793f03
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 19:59:08 2023 +0800

    fix

commit 659f503
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 18:59:49 2023 +0800

    fix merge

commit a259cc5
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 18:54:10 2023 +0800

    fix

commit d6eb31f
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 18:18:02 2023 +0800

    fix

commit 2650679
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 16:31:11 2023 +0800

    fix

commit 5bfb9ec
Merge: c5279c0 08a8af0
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 16:19:14 2023 +0800

    Merge branch 'master' into FR_canonically

commit c5279c0
Author: negiizhao <[email protected]>
Date:   Mon Aug 7 02:47:06 2023 +0800

    lint

commit 19a377f
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 16:57:10 2023 +0800

    lint

commit 048b120
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 15:43:32 2023 +0800

    fix counterexamples

commit 94663ee
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 14:22:22 2023 +0800

    lint style

commit 426dd03
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 14:00:46 2023 +0800

    refactor: make `CanonicallyOrdered...` mixin

    I think this is the proposed refactor.

    However it seems that all things get slower... :(

    Need more love to speed it up.
@FR-vdash-bot
fix
bea3ff0
@FR-vdash-bot
fixfixfix
c24d120
@FR-vdash-bot
remove ancient fixes
f7dfbca
@FR-vdash-bot
shake & lint
ac14b47
@FR-vdash-bot
style
9e571ae
@FR-vdash-bot
remove ancient fixes
ffb2b14
@FR-vdash-bot
Merge branch 'master' into FR_canonically_retry
a200e49
@FR-vdash-bot
Merge branch 'master' into FR_canonically_retry
2028556
@FR-vdash-bot
fix
c7a99cd
@FR-vdash-bot
fix
51def2a
@FR-vdash-bot
Merge branch 'master' into FR_canonically_retry
1542e4e
@FR-vdash-bot
fix
5ee9202
@FR-vdash-bot
fix
33f661d
@FR-vdash-bot
fix
1d3e479
@FR-vdash-bot
fix
283a50c
@FR-vdash-bot
fix
19de397
@FR-vdash-bot
fix
fcba328
@FR-vdash-bot
shake
d729855
@FR-vdash-bot
shake Mathlib.Algebra.Order.Ring.Nat
48e4de6
@FR-vdash-bot
reduce diffs
78a4056
@FR-vdash-bot
fix
6c63912
@FR-vdash-bot
fix
0cdcc93
@FR-vdash-bot
shake
194715e
@FR-vdash-bot
lint
633ee02
@FR-vdash-bot
remove a bad instance
3cbc9a3
@FR-vdash-bot
not shortcuts now
67a9f17
@FR-vdash-bot
fix merge
be85fcb
@FR-vdash-bot
remove ancient fixes (instance priority)
7d6bbf8
@FR-vdash-bot
examples should be removed
c303c30
@FR-vdash-bot FR-vdash-bot added t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Jan 9, 2025
@FR-vdash-bot FR-vdash-bot mentioned this pull request Jan 9, 2025
Open
1 task
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 9, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 9, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-order Order theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@FR-vdash-bot @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant