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.

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

[ refactor ] Revise definitions, consequences, and use, of Algebra.Definitions.(Almost)*Cancellative #2573

Open
wants to merge 39 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
4f1245b
refactor: revise the definitions
jamesmckinna Jan 20, 2025
b64f1e1
refactor: knock-on `Consequences`
jamesmckinna Jan 20, 2025
a77cf6e
update `README` to reflect intended milestone
jamesmckinna Jan 20, 2025
7b09efd
refactor: knock-on `Algebra.Properties.CancellativeCommutativeSemiring`
jamesmckinna Jan 20, 2025
776ff3d
refactor: tighten imports
jamesmckinna Jan 20, 2025
7e11c26
tidy up
jamesmckinna Jan 20, 2025
a3168a2
refactor: cosmetic redefinition
jamesmckinna Feb 6, 2025
1aa78f3
refactor: add definitions and consequences
jamesmckinna Feb 6, 2025
c75c12a
fix: oops!
jamesmckinna Feb 6, 2025
8d9f167
refactor: add `*-almostCancelʳ-≡`
jamesmckinna Feb 6, 2025
cbc33e8
refactor: tweak `import`s
jamesmckinna Feb 6, 2025
63694db
refactor: `breaking` rectify lemma statement
jamesmckinna Feb 6, 2025
4049a7b
refactor: cosmetic
jamesmckinna Feb 6, 2025
a46af5b
refactor: cosmetic; dollar application slows down typechecker conside…
jamesmckinna Feb 6, 2025
9a14b70
Merge branch 'master' into issue1436
jamesmckinna Feb 6, 2025
d06f0a9
refactor: avoid `with` if possible
jamesmckinna Feb 9, 2025
4bd8a7f
refactor: introduce `At` lemma factorisation
jamesmckinna Feb 9, 2025
05a11e9
`CHANGELOG`
jamesmckinna Feb 9, 2025
5e9ac7c
refactor: use `instance`s
jamesmckinna Feb 10, 2025
8eea456
refactor: knock-on
jamesmckinna Feb 10, 2025
30299f1
refactor: use `Data.Sum.Base` operations instead of `with`
jamesmckinna Feb 10, 2025
22f2ca7
Merge branch 'agda:master' into issue1436
jamesmckinna Feb 10, 2025
1fbd51a
fix: take these edits to a separate PR
jamesmckinna Feb 10, 2025
d6a461b
fix: take these edits to a separate PR
jamesmckinna Feb 10, 2025
c2e14ef
refactor: change order of parametrisation
jamesmckinna Feb 10, 2025
6ceb7a7
fix: `CHANGELOG`
jamesmckinna Feb 10, 2025
44ba20c
refactor: `import`s
jamesmckinna Feb 11, 2025
770b223
refactor: streamline, using `Data.Sum.Base.map₂`
jamesmckinna Feb 11, 2025
0747e48
refactor: streamline; deprecate already exported definition
jamesmckinna Feb 11, 2025
e12eeb5
refactor: remove one more `import`
jamesmckinna Feb 11, 2025
e5c47f3
refactor: remove one more `import`
jamesmckinna Feb 11, 2025
ad0f4b7
fix: add missing deprecation
jamesmckinna Feb 11, 2025
79dff47
Merge branch 'master' into issue1436
jamesmckinna Feb 18, 2025
bd6c6d9
Merge branch 'master' into issue1436
jamesmckinna Feb 19, 2025
2750704
Merge branch 'agda:master' into issue1436
jamesmckinna Feb 21, 2025
ed940bb
Merge branch 'master' into issue1436
jamesmckinna Feb 27, 2025
80a9aea
fix: explicit `import` policy returns to bite!
jamesmckinna Feb 27, 2025
db5d845
Merge branch 'master' into issue1436
jamesmckinna Mar 24, 2025
e27d1cb
fix: reverted change
jamesmckinna Mar 24, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Merge branch 'agda:master' into issue1436
jamesmckinna authored Feb 21, 2025

Verified

This commit was signed with the committer’s verified signature.
scala-steward Scala Steward
commit 275070475076b469a677a47121e4e39a5d7a1345

This merge commit was added into this branch cleanly.

There are no new changes to show, but you can still view the diff.