Fast-forward v2.0-release (branch) to v2.0 (tag) #2856
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality`
* missing comma! * corrected reference to `README.Design.Decidability` * typo: capitalisation * updated `installation-guide` * added word to `NonZero` section heading * Run workflows on any PR * Add merge-group trigger to workflows --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
* Make decdable versions of sublist functions the default * Remove imports Bool.Properties * Address comments
* [ admin ] dev playground * [ fix agda#1743 ] move README to doc/ directory * [ fix ] whitespace violations * [ ci ] update to cope with new doc/ directory * [ cleanup ] remove stale reference to travis.yml * [ admin ] update README-related instructions * [ admin ] fix build badges * [ fix ] `make test` build * Moved contents of notes/ to doc/ * Added CHANGELOG entry --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
…ME.md`... (agda#2197) * fix link to `installation-guide` * catching another reference to `notes/` * note on instance brackets * `HACKING` guide * added Gurmeet Singh's changes * [ fix ] links in README.md --------- Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Connex allows both relations to hold, so the old comment was wrong.
…gda#2205) * deprecating `isPropositional` * tighten `import`s * bumped Agda version number in comment
…Composite` cf. agda#2180 (agda#2181) * definition of `Irreducible`; refactoring of `Prime` and `Composite` * tidying up old cruft * knock-on consequences: `Coprimality` * considerable refactoring of `Primality` * knock-on consequences: `Coprimality` * refactoring: no appeal to `Data.Nat.Induction` * refactoring: renamed `SmoothAt` and its constructor; added pattern synonym; proved `Decidable Irreducible`; misc. tweaks * knock-on consequences: `Coprimality` * refactoring: removed `NonZero` analysis; misc. tweaks * knock-on consequences: `Coprimality`; tightened `import`s * knock-on consequences: `Coprimality`; tightened `import`s * refactoring: every number is `1-rough` * knock-on consequences: `Coprimality`; use of smart constructor * refactoring: every number is `0-rough`; streamlining; inverse to `prime`; documentation * attempt to optimise for a nearly-common case pseudo-constructor * fiddling now * refactoring: better use of `primality` API * `Rough` is bounded * removed unnecessary implicits * comment * refactoring: comprehensive shift over to `NonTrivial` instances * refactoring: oops! * tidying up: removed infixes * tidying up: restored `rough⇒≤` * further refinements; added `NonTrivial` proofs * tidying up * moving definitions to `Data.Nat.Base` * propagated changes; many more explicit s required? * `NonTrivial` is `Recomputable` * all instances of `NonTrivial` now irrelevant; weird to need `NonTrivial 2` explicitly * tidying up `Coprimality`, eg with `variable`s * `NonTrivial` is `Decidable` * systematise proofs of `Decidable` properties via the `UpTo` predicates * explicit quantifier now in `composite≢` * Nathan's simplification * interaction of `NonZero` and `NonTrivial` instances * divisor now a record field; final lemmas: closure under divisibility; plus partial `CHANGELOG` entries * '(non-)instances' become '(counter-)examples' * stylistics * removed `k` as a variable/parameter * renamed fields and smart constructors * moved smart constructors; made a local definition * tidying up * refactoring per review comments: equivalence of `UpTo` predicates; making more things `private` * tidying up: names congruent to ordering relation * removed variable `k`; removed old proof in favour of new one with `NonZero` instance * removed `recomputable` in favour of a private lemma * regularised use of instance brackets * made instances more explicit * made instances more explicit * blank line * made `nonTrivial⇒nonZero` take an explicit argument in lieu of being able to make it an `instance` * regularised use of instance brackets * regularised use of instance brackets * trimming * tidied up `Coprimality` entries * Make HasBoundedNonTrivialDivisor infix * Make NonTrivial into a record to fix instance resolution bug * Move HasNonTrivialDivisor to Divisibility.Core and hide UpTo lemmas * Rearrange file to follow standard ordering of lemmas in the rest of the library * Move UpTo predicates into decidability proofs * No-op refactoring to curb excessively long lines * Make a couple of names consistent with style-guide * new definition of `Prime` * renamed fundamental definition * one last reference in `CHANGELOG` * more better words; one fewer definition * tidied up `Definitions` section; rejigged order of proofs of properties to reflect definitional order * refactored proof of `prime⇒irreducible` * finishing touches * missing lemma from irrelevant instance list * regularised final proof to use `contradiction` * added fixity `infix 10` * added fixity `infix 10`; made `composite` a pattern synonym; knock-on improvements * comprehensive `CHNAGELOG` entry; whitespace fixes * Rename 1<2+ to sz<ss * Rename hasNonTrivialDivisor relation * Updated CHANGELOG --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
* Fix names in IsSemilattice * Add reference to changes to Semilattice to CHANGELOG
* Fix deprecated modules * [ ci ] Also build deprecated modules * [ ci ] ignore user warnings in test * [ ci ] fix filtering logic Deprecation and safety are not the same thing --------- Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
* Final admin changes for v2.0 release * Fix Agda versions
MatthewDaggitt
approved these changes
Nov 3, 2025
Contributor
|
Nice spot, not sure how that happened... |
Contributor
Author
|
Oops it looks like the commits got squashed? |
MatthewDaggitt
added a commit
that referenced
this pull request
Nov 3, 2025
This reverts commit 381b996.
Contributor
|
Eek yes. I'll back them out and merge them manually. |
Contributor
|
Right, I've rebased and forced push. They should all be there! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fast-forward v2.0-release (branch) to v2.0 (tag) because the branch is behind the tag.