Merge v2.1.1 into `master` (#2473) * Bump stdlib and agda version in installation guide (#2027) * Simplify more `Data.Product` imports to `Data.Product.Base` (#2036) * Simplify more `Data.Product` import to `Data.Product.Base` * Simplify more `Data.Product` import to `Data.Product.Base` * Indent * Wrapping Comments & Fixing Code Delimiters (#2015) * Add new pattern synonym `divides-refl` to `Data.Nat.Divisibility.Core` * Simplify more `Relation.Binary` imports (#2034) * Rename and deprecate `excluded-middle` (#2026) * Simplified `String` imports (#2016) * Change `Function.Definitions` to use strict inverses (#1156) * Proofs `take/drop/head -map-commute` added to Data.List.Properties (#1986) * Simplified `Vec` import (#2018) * More `Data.Product` simplifications (#2039) * Added Unnormalised Rational Field Structure (#1959) * More simplifications for `Relation.Binary` imports (#2038) * Move just a few more things over to new Function hierarchy. (#2044) * Final `Data.Product` import simplifications (#2052) * Added properties of Heyting Commutative Ring (#1968) * Add more properties for `xor` (#2035) * Additional lemmas about lists and vectors (#2020) * Removed redundant `import`s from `Data.Bool.Base` (#2062) * Tidying up `Data.String` (#2061) * More `Relation.Binary` simplifications (#2053) * Add `drop-drop` in `Data.List.Properties` (#2043) * Rename `push-function-into-if` * agda-stdlib-utils/AllNonAsciiChars: use List1.head instead of List.head * Bump resolvers in stack-{9.4.5,9.6.2}.yaml * Bump Haskell CI to GHC 9.8.0 and 9.4.6; allow text-2.1 * Rename `take-drop-id` and `take++drop` (#2069) A useful improvement to consistency of names, * Add `find`, `findIndex`, and `findIndices` for `Data.List` (#2042) * `find*` functions for `Data.List` both decidable predicate and boolean function variants * Back to `Maybe.map` * New type for findIndices * Add comments * Respect style guide --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Final `Relation.Binary` simplifications (#2068) * Spellchecked `CHANGELOG` (#2078) * #2075: Remove symmetry assumption from lexicographic well-foundedness (#2077) * Make sure RawRing defines rawRingWithoutOne (#1967) * Direct products and minor fixes (#1909) * Refine imports in `Reflection.AST` (#2072) * Add some `_∷ʳ_` properties to `Data.Vec.Properties` (#2041) * Monadic join (#2079) * Move `≡-setoid` to `Function.Indexed.Relation.Binary.Equality` (#2047) * Making (more) arguments implicit in lexicographic ordering lemmas * `WellFounded` proofs for transitive closure (#2082) * Add properties of Vector operations `reverse`, `_++_` and `fromList` (#2045) * Rename `minor changes` section in CHANGELOG * Improve implementation of `splitAt`, `take` and `drop` in `Data.List`. (#2056) * Add a recursive view of `Fin n` (#1923) * Use new style `Function` hierarchy everywhere. (#1895) * Fix typo and whitespace violation (#2104) * Add Kleene Algebra morphism with composition and identity construct (#1936) * Added foldr of permutation of Commutative Monoid (#1944) * Add `begin-irrefl` reasoning combinator (#1470) * Refactor some lookup and truncation lemmas (#2101) * Add style-guide note about local suffix (#2109) * Weakened pre-conditions of grouped map lemmas (#2108) * Undeprecate inspect idiom (#2107) * Add some lemmas related to renamings and substitutions (#1750) * Proof of the Binomial Theorem for `(Commutative)Semiring` [supersedes #1287] (#1928) * Modernise `Relation.Nullary` code (#2110) * Add new fixities (#2116) Co-authored-by: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com> * Adds setoid export to `Algebra.Bundles.SemiringWithoutOne` * #453: added `Dense` relations and `DenseLinearOrder` (#2111) * Rectifies the negated equality symbol in `Data.Rational.Unnormalised.*` (#2118) * Sync insert, remove, and update functionalities for `List` and `Vec` (#2049) * De-symmetrising `Relation.Binary.Bundles.Preorder._∼_` (#2099) * Redefines `Data.Nat.Base._≤″_` (#1948) * Sync `iterate` and `replicate` for `List` and `Vec` (#2051) * Changes explicit argument `y` to implicit in `Induction.WellFounded.WfRec` (#2084) * Re-export numeric subclass instances * Revert "Re-export numeric subclass instances" This reverts commit 91fd951c117311b2beb2db4a582c4f152eac787d. * Add (propositional) equational reasoning combinators for vectors (#2067) * Strict and non-strict transitive property names (#2089) * Re-export numeric subclass instances (#2122) * Added Irreflexivity and Asymmetry of WellFounded Relations (#2119) * Fix argument order of composition operators (#2121) * Make size parameter on 'replicate' explicit (#2120) * [fixes #2130] Moving `Properties.HeytingAlgebra` from `Relation.Binary` to `Relation.Binary.Lattice` (#2131) * [fixes #2127] Fixes #1930 `import` bug (#2128) * [fixes #1214] Add negated ordering relation symbols systematically to `Relation.Binary.*` (#2095) * Refactoring (inversion) properties of `_<_` on `Nat`, plus consequences (#2000) * Bump CI tests to Agda-2.6.4 (#2134) * Remove `Algebra.Ordered` (#2133) * [ fix ] missing name in LICENCE file (#2139) * Add new blocking primitives to `Reflection.TCM` (#1972) * Change definition of `IsStrictTotalOrder` (#2137) * Add _<$>_ operator for Function bundle (#2144) * [ fix #2086 ] new web deployment strategy (#2147) * [ admin ] fix sorting logic (#2151) With the previous script we were sorting entries of the form html/vX.Y.Z/index.html but the order is such that vX.Y/ < vX.Y.Z/ and so we were ending up with v1.7 coming after v1.7.3. This fixes that by using sed to get rid of the html/ prefix and the /index.html suffix before the sorting phase. * Add coincidence law to modules (#1898) * Make reasoning modular by adding new `Reasoning.Syntax` module (#2152) * Fixes typos identified in #2154 (#2158) * tackles #2124 as regards `case_return_of_` (#2157) * Rename preorder ~ relation reasoning combinators (#2156) * Move ≡-Reasoning from Core to Properties and implement using syntax (#2159) * Add consistent deprecation warnings to old function hierarchy (#2163) * Rename symmetric reasoning combinators. Minimal set of changes (#2160) * Restore 'return' as an alias for 'pure' (#2164) * [ fix #2153 ] Properly re-export specialised combinators (#2161) * Connect `LeftInverse` with (`Split`)`Surjection` (#2054) * Added remaining flipped and negated relations to binary relation bundles (#2162) * Tidy up CHANGELOG in preparation for release candidate (#2165) * Spellcheck CHANGELOG (#2167) * spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality` * Fixed Agda version typo in README (#2176) * Fixed in deprecation warning for `<-transˡ` (#2173) * Bump Haskell CI (original!) to latest minor GHC versions (#2187) * [fixes #2175] Documentation misc. typos etc. for RC1 (#2183) * 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 * [fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185) * regularise and specify/systematise, the conventions for symbol usage * typos/revisions * Move `T?` to `Relation.Nullary.Decidable.Core` (#2189) * Move `T?` to `Relation.Nullary.Decidable.Core` * Var name fix * Some refactoring * Fix failing tests and address remaining comments * Fix style-guide * Make decidable versions of sublist functions the default (#2186) * Make decdable versions of sublist functions the default * Remove imports Bool.Properties * Address comments * [ fix #1743 ] move README to `doc/` directory (#2184) * [ admin ] dev playground * [ fix #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 * documentation: fix link to `installation-guide`, `README.agda`, `README.md`... (#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 * easy deprecation; leftover from `v1.6` perhaps? (#2203) * fix Connex comment (#2204) Connex allows both relations to hold, so the old comment was wrong. * Add `Function.Consequences.Setoid` (#2191) * Add Function.Consequences.Setoid * Fix comment * Fix re-export bug * Finally fixed bug I hope * Removed rogue comment * More tidying up * Deprecating `Relation.Binary.PropositionalEquality.isPropositional` (#2205) * deprecating `isPropositional` * tighten `import`s * bumped Agda version number in comment * definition of `Irreducible` and `Rough`; refactoring of `Prime` and `Composite` cf. #2180 (#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 * [fixes #2168] Change names in `Algebra.Consequences.*` to reflect `style-guide` conventions (#2206) * fixes issue #2168 * added more names for deprecation, plus `hiding` them in `Propositional` * Add biased versions of Function structures (#2210) * Fixes #2166 by fixing names in `IsSemilattice` (#2211) * Fix names in IsSemilattice * Add reference to changes to Semilattice to CHANGELOG * remove final references to `Category.*` (#2214) * Fix #2195 by removing redundant zero from IsRing (#2209) * Fix #2195 by removing redundant zero from IsRing * Moved proofs eariler to IsSemiringWithoutOne * Updated CHANGELOG * Fix bug * Refactored Properties.Ring * Fix renaming * Fix #2216 by making divisibility definitions records (#2217) * Fix #2216 by making divisibility definitions records * remove spurious/ambiguous `import` --------- Co-authored-by: jamesmckinna * Fix deprecated modules (#2224) * 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 * Final admin changes for v2.0 release (#2225) * Final admin changes for v2.0 release * Fix Agda versions * Fix typo in raise deprecation message (#2226) * Setup for v2.1 (#2227) * Added tabulate+< (#2190) * added tabulate+< * renamed tabulate function --------- Co-authored-by: Guilherme Co-authored-by: MatthewDaggitt * Added pointwise and catmaybe in Lists (#2222) * added pointwise and catmaybe * added pointwise to any * added cat maybe all * changed pointwise definition * changed files name * fixed changelogs and properties * changed Any solution * changed pointwise to catMaybe --------- Co-authored-by: Guilherme Co-authored-by: MatthewDaggitt * [fixes #1711] Refactoring `Data.Nat.Divisibility` and `Data.Nat.DivMod` (#2182) * added new definitions to `_∣_` * `CHANGELOG` * don't declare `quotient≢0` as an `instance` * replace use of `subst` with one of `trans` * what's sauce for the goose... * switch to a `rewrite`-based solution... * tightened `import`s * simplified dependenciess * simplified dependencies; `CHANGELOG` * removed `module` abstractions * delegated proof of `quotient≢0` to `Data.Nat.Properties` * removed redundant property * cosmetic review changes; others to follow * better proof of `quotient>1` * `where` clause layout * leaving in the flipped equality; moved everything else * new lemmas moved from `Core`; knock-on consequences; lots of tidying up * tidying up; `CHANGELOG` * cosmetic tweaks * reverted to simple version * problems with exporting `quotient` * added last lemma: defining equation for `_/_` * improved `CHANGELOG` * revert: simplified imports * improved `CHANGELOG` * endpoint of simplifying the proof of `*-pres-∣` * simplified the proof of `n/m≡quotient` * simplified the proof of `∣m+n∣m⇒∣n` * simplified the proof of `∣m∸n∣n⇒∣m` * simplified `import`s * simplified a lot of proofs, esp. wrt `divides-refl` and `NonZero` reasoning * simplified more proofs, esp. wrt `divides-refl` reasoning * simplified `import`s * moved `equalityᵒ` proof out of `Core` * `CHANGELOG` * temporary fix: further `NonZero` refactoring advised! * regularised use of instance brackets * further instance simplification * further streamlining * tidied up `CHANGELOG` * simplified `NonZero` pattern matching * regularised use of instance brackets * simplified proof of `/-*-interchange` * simplified proof of `/-*-interchange` * ... permitting the migration of `*-pres-∣` to `Data.Nat.Divisibility` * tweaked proof of `/-*-interchange` * narrowed `import`s * simplified proof; renamed new proofs * Capitalisation * streamlined `import`s; streamlined proof of decidability * spurious duplication after merge * missing symbol import * replaced one use of `1 < m` with `{{NonTrivial m}}` * fixed `CHANGELOG` * removed use of identifier `k` * refactoring: more use of `NonTrivial` instances * knock-on consequences: simplified function * two new lemmas * refactoring: use of `connex` in proofs * new lemmas about `pred` * new lemmas about monus * refactoring: use of the new properties, simplifying pattern analysis * whitespace * questionable? revision after comments on #2221 * silly argument name typo; remove parens * tidied up imports of `Relation.Nullary` * removed spurious `instance` * localised appeals to `Reasoning` * further use of `variable`s * tidied up `record` name in comment * cosmetic * reconciled implicit/explicit arguments in various monus lemmas * fixed knock-on change re monus; reverted change to `m/n Co-authored-by: MatthewDaggitt * fixes issue #2237 (#2238) * fixes issue #2237 * leftover from #2182: subtle naming 'bug'/anomaly * Bring back a convenient short-cut for infix Func (#2239) * Bring back a convenient short-cut for infix Func * change name as per suggestion from Matthew * propagate use of shortcut to where it increases readability * Revert "propagate use of shortcut to where it increases readability" This reverts commit debfec19a0b6ad93cadce4e88f559790b287a316. * Move definitions up. Fix comments. * fixes #2234 (#2241) * Update `HACKING` (#2242) * added paragraph on coupled contributions * typo * Bring back shortcut [fix CHANGELOG] (#2246) * Bring back a convenient short-cut for infix Func * change name as per suggestion from Matthew * propagate use of shortcut to where it increases readability * Revert "propagate use of shortcut to where it increases readability" This reverts commit debfec19a0b6ad93cadce4e88f559790b287a316. * Move definitions up. Fix comments. * fix CHANGELOG to report the correct syntax. * fix toList-replicate's statement about vectors (#2261) * Remove all external use of `less-than-or-equal` beyond `Data.Nat.*` (#2256) * removed all external use of `less-than-or-equal` beyond `Data.Nat.*` * use of `variable`s * Raw modules bundles (#2263) * Raw bundles for modules * Export raw bundles from module bundles * Update chnagelog * Remove redundant field * Reexport raw bundles, add raw bundles for zero * Add missing reexports, raw bundles for direct product * Raw bundles for tensor unit * Update changelog again * Remove unused open * Fix typo * Put a few more definitions in the fake record modules for RawModule and RawSemimodule * Parametrize module morphisms by raw bundles (#2265) * Index module morphisms by raw bundles * Use synonyms for RawModule's RawBimodule etc * Update changelog * Update constructed morphisms * Fix Algebra.Module.Morphism.ModuleHomomorphism * add lemma (#2271) * additions to `style-guide` (#2270) * added stub content on programming idioms * added para on qualified import names * fixes issue #1688 (#2254) * Systematise relational definitions at all arities (#2259) * fixes #2091 * revised along the lines of @MatthewDaggitt's suggestions --------- Co-authored-by: MatthewDaggitt * lemmas about semiring structure induced by `_× x` (#2272) * tidying up proofs of, and using, semiring structure induced by `_× x` * reinstated lemma about `0#` * fixed name clash * added companion lemma for `1#` * new lemma, plus refactoring * removed anonymous `module` * don't inline use of the lemma * revised deprecation warning * Qualified import of `Data.Nat` fixing #2280 (#2281) * `Algebra.Properties.Semiring.Binomial` * `Codata.Sized.Cowriter` * `Data.Char.Properties` * `Data.Difference*` * `Data.Fin.*` * `Data.Float.Properties` * `Data.Graph.Acyclic` * `Data.Integer.Divisibility`: still need to disambiguate `Divisibility`? * `Data.List.Extrema.Nat` * `Data.List.Relation.Binary.*` * `Data.Nat.Binary.*` * `Data.Rational.Base` * `Data.String` * `Data.Vec.*` * `Data.Word` * `Induction.Lexicographic` * `Reflection.AST` * `Tactic.*` * `Text.*` * Fix import in README.Data.Fin.Substitution.UntypedLambda (#2279) Also import this module in doc/README.agda so that it is covered by CI. Closes #2278. * Qualified import of reasoning modules fixing #2280 (#2282) * `Data.List.Relation.Relation.Binary.BagAndSetEquality` * `Relation.Binary.Reasoning.*` * preorder reasoning * setoid reasoning * alignment * Qualified import of `Data.Product.Base` fixing #2280 (#2284) * Qualified import of `Data.Product.Base as Product` * more modules affected * standardise use of `Properties` modules (#2283) * missing code endquote (#2286) * manual fix for #1380 (#2285) * fixed `sized-types` error in orphan module (#2295) * Qualified import of `PropositionalEquality` etc. fixing #2280 (#2293) * Qualified import of `PropositionalEquality` fixing #2280 * Qualified import of `PropositionalEquality.Core` fixing #2280 * Qualified import of `HeterogeneousEquality.Core` fixing #2280 * simplified imports; fixed `README` link * simplified imports * Added functional vector permutation (#2066) * added functional vector permutation * added one line to CHANGELOG * added permutation properties * Added Base to imports Co-authored-by: Nathan van Doorn * Added Base to import Co-authored-by: Nathan van Doorn * Added core to import Co-authored-by: Nathan van Doorn * added definitions * removed unnecessary zs * renamed types in changelog * removed unnecessary code * added more to changelog * added end of changelog --------- Co-authored-by: Nathan van Doorn Co-authored-by: Guilherme * Nagata's "idealization of a module" construction (#2244) * Nagata's construction * removed redundant `zero` * first round of Jacques' review comments * proved the additional properties * some of Matthew's suggestions, plus more vertical whitespace, less horizontal; more comments * Matthew's suggestion: using `private` modules * Matthew's suggestion: lifting out left-/right- sublemmas * standardised names, as far as possible * Matthew's suggestion: lifting out left-/right- sublemmas * fixed constraint problem with ambiguous symbol; renamed ideal lemmas * renamed module * renamed module in `CHANGELOG` * added generalised annihilation lemma * typos * use correct rexported names * now as a paramterised module instead * or did you intend this? * fix whitespace * aligned one step of reasoning * more re-alignment of reasoning steps * more re-alignment of reasoning steps * Matthew's review comments * blanklines * Qualified import of `Data.Sum.Base` fixing #2280 (#2290) * Qualified import of `Data.Sum.Base as Sum` * resolve merge conflict in favour of #2293 * [ new ] associativity of Appending (#2023) * [ new ] associativity of Appending * Removed unneeded variable * Renamed Product module --------- Co-authored-by: MatthewDaggitt * [ new ] symmetric core of a binary relation (#2071) * [ new ] symmetric core of a binary relation * [ fix ] name clashes * [ more ] respond to McKinna's comments * [ rename ] fields to lhs≤rhs and rhs≤lhs * [ more ] incorporate parts of McKinna's review * [ minor ] remove implicit argument application from transitive * [ edit ] pull out isEquivalence and do some renaming * [ minor ] respond to easy comments * [ refactor ] remove IsProset, and move Proset to main hierarchy * Eliminate Proset * Fixed CHANGELOG typo --------- Co-authored-by: MatthewDaggitt * refactored proofs from #2023 (#2301) * Qualified imports in `Data.Integer.Divisibility` fixing #2280 (#2294) * fixing #2280 * re-export constructor via pattern synonym * updated `README` * refactor: better disambiguation; added a note in `CHANGELOG` * guideline for `-Reasoning` module imports (#2309) * Function setoid is back. (#2240) * Function setoid is back. * make all changes asked for in review * fix indentation * Style guide: avoid `renaming` on qualified import cf. #2294 (#2308) * recommendation from #2294 * spellcheck * comma --------- Co-authored-by: MatthewDaggitt * make `mkRawMonad` and `mkRawApplicative` universe-polymorphic (#2314) * make `mkRawMonad` and `mkRawApplicative` universe-polymorphic * fix unresolved metas --------- Co-authored-by: Gan Shen * Some properties of upTo and downFrom (#2316) * Some properties of upTo and downFrom * Rename things per review comments * Fix changelog typo * Tidy up `README` imports #2280 (#2313) * tidying up `README` imports * address Matthew's review comments * Add unique morphisms from/to `Initial` and `Terminal` algebras (#2296) * added unique morphisms * refactored for uniformity's sake * exploit the uniformity * add missing instances * finish up, for now * `CHANGELOG` * `CHANGELOG` * `TheMorphism` * comment * comment * comment * `The` to `Unique` * lifted out istantiated `import` * blank line * note on instantiated `import`s * parametrise on the `Raw` bundle * parametrise on the `Raw` bundle * Rerranged to get rid of lots of boilerplate --------- Co-authored-by: MatthewDaggitt * Setoid version of indexed containers. (#1511) * Setoid version of indexed containers. Following the structure for non-indexed containers. * An example for indexed containers: multi-sorted algebras. This tests the new setoid version of indexed containers. * Brought code up to date * Added CHANGELOG entry --------- Co-authored-by: MatthewDaggitt * 'No infinite descent' for (`Acc`essible elements of) `WellFounded` relations (#2126) * basic result * added missing lemma; is there a better name for this? * renamed lemma * final tidying up; `CHANGELOG` * final tidying up * missing `CHANGELOG` entry * `InfiniteDescent` definition and proof * revised `InfiniteDescent` definition and proof * major revision: renames things, plus additional corollaries * spacing * added `NoSmallestCounterExample` principles for `Stable` predicates * refactoring; move `Stable` to `Relation.Unary` * refactoring; remove explicit definition of `CounterExample` * refactoring; rename qualified `import` * [fixes #2130] Moving `Properties.HeytingAlgebra` from `Relation.Binary` to `Relation.Binary.Lattice` (#2131) * [fixes #2127] Fixes #1930 `import` bug (#2128) * [fixes #1214] Add negated ordering relation symbols systematically to `Relation.Binary.*` (#2095) * Refactoring (inversion) properties of `_<_` on `Nat`, plus consequences (#2000) * Bump CI tests to Agda-2.6.4 (#2134) * Remove `Algebra.Ordered` (#2133) * [ fix ] missing name in LICENCE file (#2139) * Add new blocking primitives to `Reflection.TCM` (#1972) * Change definition of `IsStrictTotalOrder` (#2137) * Add _<$>_ operator for Function bundle (#2144) * [ fix #2086 ] new web deployment strategy (#2147) * [ admin ] fix sorting logic (#2151) With the previous script we were sorting entries of the form html/vX.Y.Z/index.html but the order is such that vX.Y/ < vX.Y.Z/ and so we were ending up with v1.7 coming after v1.7.3. This fixes that by using sed to get rid of the html/ prefix and the /index.html suffix before the sorting phase. * Add coincidence law to modules (#1898) * Make reasoning modular by adding new `Reasoning.Syntax` module (#2152) * Fixes typos identified in #2154 (#2158) * tackles #2124 as regards `case_return_of_` (#2157) * Rename preorder ~ relation reasoning combinators (#2156) * Move ≡-Reasoning from Core to Properties and implement using syntax (#2159) * Add consistent deprecation warnings to old function hierarchy (#2163) * Rename symmetric reasoning combinators. Minimal set of changes (#2160) * Restore 'return' as an alias for 'pure' (#2164) * [ fix #2153 ] Properly re-export specialised combinators (#2161) * Connect `LeftInverse` with (`Split`)`Surjection` (#2054) * Added remaining flipped and negated relations to binary relation bundles (#2162) * Tidy up CHANGELOG in preparation for release candidate (#2165) * Spellcheck CHANGELOG (#2167) * spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality` * Fixed Agda version typo in README (#2176) * Fixed in deprecation warning for `<-transˡ` (#2173) * Bump Haskell CI (original!) to latest minor GHC versions (#2187) * [fixes #2175] Documentation misc. typos etc. for RC1 (#2183) * 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 * [fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185) * regularise and specify/systematise, the conventions for symbol usage * typos/revisions * Move `T?` to `Relation.Nullary.Decidable.Core` (#2189) * Move `T?` to `Relation.Nullary.Decidable.Core` * Var name fix * Some refactoring * Fix failing tests and address remaining comments * Fix style-guide * Make decidable versions of sublist functions the default (#2186) * Make decdable versions of sublist functions the default * Remove imports Bool.Properties * Address comments * new `CHANGELOG` * resolved merge conflict * resolved merge conflict, this time * revised in line with review comments * tweaked `export`s; does that fix things now? * Fix merge mistake * Refactored to remove a indirection and nested modules * Touch up names * Reintroduce anonymous module for descent * cosmetics asper final comment --------- Co-authored-by: MatthewDaggitt Co-authored-by: G. Allais Co-authored-by: Amélia Co-authored-by: Nathan van Doorn Co-authored-by: James Wood Co-authored-by: Andreas Abel * Add new operations (cf. `RawQuasigroup`) to `IsGroup` (#2251) * added new operations to `IsGroup` * fixed notations * fixed `CHANGELOG` * refactoring `Group` properties: added `isQuasigroup` and `isLoop` * refactoring `*-helper` lemmas * fixed `CHANGELOG` * lemma relating quasigroup operations and `Commutative` property * simplified proof * added converse property to \¬Algebra.Properties.AbelianGroup` * moved lemma * indentation; congruence lemmas * untangled operation definitions * untangled operation definitions in `CHANGELOG` * fixed names * reflexive reasoning; tightened imports * refactoring to push properties into `Loop`, and re-export them from there and `Quasigroup` * further refactoring * final refactoring * Minor naming tweaks --------- Co-authored-by: MatthewDaggitt * Add prime factorization and its properties (#1969) * Add prime factorization and its properties * Add missing header comment I'd missed this when copy-pasting from my old code in a separate repo * Remove completely trivial lemma * Use equational reasoning in quotient|n proof * Fix typo in module header * Factorization => Factorisation * Use Nat lemma in extend-|/ * [ cleanup ] part of the proof * [ cleanup ] finishing up the job * [ cleanup ] a little bit more * [ cleanup ] the import list * [ fix ] header style * [ fix ] broken merge: missing import * Move Data.Nat.Rough to Data.Nat.Primality.Rough * Rename productPreserves↭⇒≡ to product-↭ * Use proof of Prime=>NonZero * Open reasoning once in factoriseRec * Rename Factorisation => PrimeFactorisation * Move wheres around * Tidy up Rough a bit * Move quotient|n to top of file * Replace factorisationPullToFront with slightly more generally useful factorisationHasAllPrimeFactors and a bit of logic * Fix import after merge * Clean up proof of 2-rough-n * Make argument to 2-rough-n implicit * Rename 2-rough-n to 2-rough * Complete merge, rewrite factorisation logic a bit Rewrite partially based on suggestions from James McKinna * Short circuit when candidate is greater than square root of product * Remove redefined lemma * Minor simplifications * Remove private pattern synonyms * Change name of lemma * Typo * Remove using list from import It feels like we're importing half the module anyway * Clean up proof * Fixes after merge * Addressed some feedback * Fix previous merge --------- Co-authored-by: Guillaume Allais Co-authored-by: MatthewDaggitt * Refactor `Data.List.Relation.Binary.BagAndSetEquality` (#2321) * easy refactorings for better abstraction * tweaking irrefutable `with` * Tidy up functional vector permutation #2066 (#2312) * added structure and bundle; tidied up * added structure and bundle; tidied up * fix order of entries * blank line * standardise `variable` names * alignment * A tweak for the cong! tactic (#2310) * ⌞_⌟ for marking spots to rewrite. * Added documentation. * In case of failure, try swapping the RHS with the LHS. Fixes ≡˘⟨ ... ⟩. * Added comments. * More clarity. Less redundancy. * Fixed performance regression. * Changelog entry. * cong!-specific combinators instead of catchTC. * Support other reasoning modules. * Clarifying comment. * Slight performance boost. * Go back to catchTC. * Fix example after merge. * Use renamed backward step. * Language tweaks. --------- Co-authored-by: MatthewDaggitt * Simplify `Data.List.Relation.Unary.Any.Properties`: remove dependency on `List.Properties` (#2323) * simplifed proof; removed dependency on `List.Properties` * corrected module long name in comment * Refactor `Data.Integer.Divisibility.Signed` (#2307) * removed extra space * refactor to introduce new `Data.Integer.Properties` * refactor proofs to use new properties; streamline reasoning * remove final blank line * first review comment: missing annotation * removed two new lemmas: `i*j≢0⇒i≢0` and `i*j≢0⇒j≢0` * Sublists: generalize disjoint-union-is-cospan to upper-bound-is-cospan (#2320) * Sublists: generalize disjoint-union-is-cospan to upper-bound-is-cospan The disjointness assumption is superfluous. * Move sublist cospan stuff to new module SubList.Propositional.Slice * CHANGELOG * Include CHANGELOG in fix-whitespace and whitespace fixes (#2325) * Fix standard-library.agda-lib (#2326) * Predicate transformers: Reconciling `Induction.RecStruct` with `Relation.Unary.PredicateTransformer.PT` (#2140) * reconciling `Induction.RecStruct` with `Relation.Unary.PredicateTransformer.PT` * relaxing `PredicateTransformer` levels * `CHANGELOG`; `fix-whitespace` * added `variable`s; plus tweaked comments` * restored `FreeMonad` * restored `Predicate` * removed linebreaks * Github action to check for whitespace violations (#2328) Co-authored-by: MatthewDaggitt * [refactor] Relation.Nulllary.Decidable.Core (#2329) * minor refactor: use Data.Unit.Polymorphic instead of an explicit Lift. * additional tweak: use contradiction where possible. * Some design documentation (here: level polymorphism) (#2322) * add some design documentation corresponding to issue #312. (Redo of bad 957) * more documentation about LevelPolymorphism * more documentation precision * document issues wrt Relation.Unary, both in design doc and in file itself. * mark variables private in Data.Container.FreeMonad (#2332) * Move pointwise equality to `.Core` module (#2335) * Closes #2331. Also makes a few changes of imports that are related. Many of the places which look like this improvement might also help use other things from `Relation.Binary.PropositionalEquality` that should *not* be moved to `.Core`. (But it might make sense to split them off into their own lighter weight module.) * don't import Data.Nullary itself since its sub-modules were already imported, just redistribute the using properly. * fix warning: it was pointing to a record that did not exist. (#2344) * Tighten imports some more (#2343) * no need to use Function when only import is from Function.Base * Use Function.Base when it suffices * use Data.Product.Base as much as possible. Make imports more precise in many of the files touched. Split an example off into a README instead of using more imports just for its sake. * more tightening of imports. * a few more tightening imports * Tighten imports (#2334) * tighten imports in some files, and make imports explicit in others. Driven by staring at a partial dependency graph. * more tightening of imports * and even more tightening of imports * some explicit for precision --------- Co-authored-by: G. Allais * [fixes #2273] Add `SuccessorSet` and associated boilerplate (#2277) * added `RawNNO` * [fix #2273] Add `NNO`-related modules * start again, fail better... * rectify names * tighten `import`s * rectify names: `CHANGELOG` --------- Co-authored-by: MatthewDaggitt * Tighten imports, last big versoin (#2347) * more tightening of imports. Mostly driven by Data.Bool, Data.Nat and Data.Char. * more tightening of imports * mostly Data.Unit * slightly tighten imports. * remove import of unused Lift) * fix all 3 things noticed by @jamesmckinna * Systematise use of `Relation.Binary.Definitions.DecidableEquality` (#2354) * systematic use of `DecidableEquality` * tweak * Added missing v1.7.3 CHANGELOG (#2356) * Improve `Data.List.Base.mapMaybe` (#2359; deprecate use of `with` #2123) (#2361) * `with`-free definitions plus tests * `CHANGELOG` * use `foldr` on @JacquesCarette 's solution * tidied up unsolved metas * factrored out comparison as removable module `MapMaybeTest` * tidied up; removed `mapMaybeTest` * tidied up; removed v2.1 deprecation section * tidy up long line * Update src/Data/List/Base.agda Co-authored-by: G. Allais * @gallais 's comments * Update src/Data/List/Base.agda Oops! Co-authored-by: G. Allais --------- Co-authored-by: G. Allais * Add a consequence of definition straight to IsCancellativeCommutativeSemiring (#2370) * Closes #2315 * whitespace * [ new ] System.Random bindings (#2368) * [ new ] System.Random bindings * [ more ] Show functions, test * [ fix ] Nat bug, more random generators, test case * [ fix ] missing file + local gitignore * [ fix ] forgot to update the CHANGELOG * Another tweak to cong! (#2340) * Disallow meta variables in goals - they break anti-unification. * Postpone checking for metas. * CHANGELOG entry, unit tests, code tweak. * Move blockOnMetas to a new Reflection.TCM.Utilities module. * Improve `Data.List.Base.unfold` (#2359; deprecate use of `with` #2123) (#2364) * `with`-free definition of `unfold` * fixed previous commit * fix #2253 (#2357) * Remove uses of `Data.Nat.Solver` from a number of places (#2337) * tighten imports in some files, and make imports explicit in others. Driven by staring at a partial dependency graph. * more tightening of imports * and even more tightening of imports * some explicit for precision * new Nat Lemmas to use instead of Solve in Data.Integer.Properties * use direct proofs instead of solver for all Nat proofs in these files * two more uses of Data.Nat.Solver for rather simple proofs, now made direct. * fix whitespace violations * remove some unneeded parens * minor fixups based on review * Relation.Binary.PropositionalEquality over-use, (#2345) * Relation.Binary.PropositionalEquality over-use, can usually be .Core and/or .Properties * unused import * another large batch of dependency cleanup, mostly cenetered on Relation.Binary.PropositionalEquality. * another big batch of making imports more precise. * last big batch. After this will come some tweaks based on reviews. * fix things pointed out in review; add CHANGELOG. * Update DecPropositional.agda Bad merge * proper merge * [ new ] IO buffering, and loops (#2367) * [ new ] IO conditionals & loops * [ new ] stdin, stdout, stderr, buffering, etc. * [ fix ] and test for the new IO primitives * [ fix ] compilation * [ fix ] more import fixing * [ done (?) ] with compilation fixes * [ test ] add test to runner * [ doc ] explain the loop * [ compat ] add deprecated stub * [ fix ] my silly mistake * [ doc ] list re-exports in CHANGELOG * [ cleanup ] imports in the Effect.Monad modules (#2371) * Add proofs to Data.List.Properties (#2355) * Add map commutation with other operations map commutes with most list operations in some way, and I initially made a section just for these proofs, but later decided to spread them into each section for consistency. * Add congruence to operations that miss it * Add flip & comm proofs to align[With] & [un]zip[With] For the case of zipWith, the existing comm proof can be provided in terms of cong and flip. For the case of unzip[With], the comm proof has little use and the flip proof is better named "swap". * Remove unbound parameter The alignWith section begins with a module _ {f g : These A B → C} where but g is only used by the first function. * Add properties for take * Proof of zip[With] and unzip[With] being inverses * fixup! don't put list parameters in modules * fixup! typo in changelog entry * fixup! use equational reasoning in place of trans * Add interaction with ++ in two more operations * fixup! foldl-cong: don't take d ≡ e * prove properties about catMaybes now that catMaybes is no longer defined in terms of mapMaybe, properties about mapMaybe need to be proven for catMaybe as well * move mapMaybe properties down see next commit (given that mapMaybe-concatMap now depends on map-concatMap, it has to be moved down) * simplify mapMaybe proofs since mapMaybe is now defined in terms of catMaybes and map, we can derive its proofs from the proofs of those rather than using induction directly --------- Co-authored-by: MatthewDaggitt * Improve `Data.List.Base` (fix #2359; deprecate use of `with` #2123) (#2365) * refactor towards `if_then_else_` and away from `yes`/`no` * reverted chnages to `derun` proofs * undo last reversion! * layout * A number of `with` are not really needed (#2363) * a number of 'with' are not really needed. Many, many more were, so left as is. * whitespace * deal with a few outstanding comments. * actually re-introduce a 'with' as it is actually clearer. * with fits better here too. * tweak things a little from review by James. * Update src/Codata/Sized/Cowriter.agda layout for readability Co-authored-by: G. Allais * Update src/Data/Fin/Base.agda layout for readability Co-authored-by: G. Allais * Update src/Data/List/Fresh/Relation/Unary/All.agda layout for readability Co-authored-by: G. Allais --------- Co-authored-by: G. Allais * [ new ] ⁻¹-anti-homo-(// | \\) (#2349) * [ new ] ¹-anti-homo‿- * Update CHANGELOG.md Co-authored-by: Nathan van Doorn * Update src/Algebra/Properties/Group.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * [ more ] symmetric lemma * [ new ] ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x --------- Co-authored-by: MatthewDaggitt Co-authored-by: Nathan van Doorn Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Add `_>>_` for `IO.Primitive.Core` (#2374) This has to be in scope for desugaring `do` blocks that don't bind intermediate results. * refactored to lift out `isEquivalence` (#2382) * `Data.List.Base.reverse` is self adjoint wrt `Data.List.Relation.Binary.Subset.Setoid._⊆_` (#2378) * `reverse` is `SelfInverse` * use `Injective` for `reverse-injective` * fixes #2353 * combinatory form * removed redundant implicits * added comment on unit/counit of the adjunction * fixes #2375 (#2377) * fixes #2375 * removed redundant `Membership` instances * fix merge conflict error * Add `Data.List.Relation.Binary.Sublist.Setoid` categorical properties (#2385) * refactor: `variable` declarations and `contradiction` * refactor: one more `contradiction` * left- and right-unit lemmas * left- and right-unit lemmas * `CHANGELOG` * `CHANGELOG` * associativity; fixes #816 * Use cong2 to save rewrites * Make splits for ⊆-assoc exact, simplifying the [] case * Simplify ⊆-assoc not using rewrite * Remove now unused private helper * fix up names and `assoc` orientation; misc. cleanup * new proofs can now move upwards * delegate proofs to `Setoid.Properties` --------- Co-authored-by: Andreas Abel * Pointwise `Algebra` (#2381) * Pointwise `Algebra` * temporary commit * better `CHANGELOG` entry? * begin removing redundant `module` implementation * finish removing redundant `module` implementation * make `liftRel` implicitly quantified * Algebra fixity (#2386) * put the fixity recommendations into the style guide * mixing fixity declaration * was missing a case * use the new case * add fixities for everything in Algebra * incorporate some suggestions for extra cases * Decidable Setoid -> Apartness Relation and Rational Heyting Field (#2194) * new stuff * forgot to add bundles for rational instance of Heyting* * one more (obvious) simplification * a few more simplifications * comments on DecSetoid properties from jamesmckinna * not working, but partially there * woo! * fix anonymous instance * fix errant whitespace * `fix-whitespace` * rectified wrt `contradiction` * rectified `DecSetoid` properties * rectified `Group` properties * inlined lemma; tidied up --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Co-authored-by: James McKinna * CI bumps: ghc 9.10, action versions, Agda to 2.6.4.3 (#2398) * Haskell CI (for GenerateEverything) and dependencies bumped to GHC 9.10.1 * CI: bump some versions, satisfy some shellcheck complaints * Refactor `Data.List.Base.scan*` and their properties (#2395) * refactor `scanr` etc. * restore `inits` etc. but lazier; plus knock-on consequences * more refactoring; plus knock-on consequences * tidy up * refactored into `Base` * ... and `Properties` * fix-up `inits` and `tails` * fix up `import`s * knock-ons * Andreas's suggestions * further, better, refactoring is possible * yet further, better, refactoring is possible: remove explicit equational reasoning! * Update CHANGELOG.md Fix deprecated names * Update Base.agda Fix deprecations * Update Properties.agda Fix deprecations * Update CHANGELOG.md Fix deprecated names * fixes #2390 (#2392) * Add the `Setoid`-based `Monoid` on `(List, [], _++_)` (#2393) * refactored from #2350 * enriched the `module` contents in response to review comments * Lists: decidability of Subset+Disjoint relations (#2399) * fixes #906 (#2401) * More list properties about `catMaybes/mapMaybe` (#2389) * More list properties about `catMaybes/mapMaybe` - Follow-up to PR #2361 - Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256) * Revert irrefutable `with`s for inductive hypotheses. * Very dependent map (#2373) * add some 'very dependent' maps to Data.Product. More documentation to come later. * and document * make imports more precise * minimal properties of very-dependen map and zipWith. Structured to make it easy to add more. * whitespace * implement new names and suggestions about using pattern-matching in the type * whitespace in CHANGELOG * small cleanup based on latest round of comments * and fix the names in the comments too. --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Improve `Data.List.Base` (fix #2359; deprecate use of with #2123) (#2366) * refactor towards `if_then_else_` * layout * `let` into `where` * Adds `Relation.Nullary.Recomputable` plus consequences (#2243) * prototype for fixing #2199 * delegate to `Relation.Nullary.Negation.Core.weak-contradiction` * refactoring: lift out `Recomputable` in its own right * forgot to add this module * refactoring: tweak * tidying up; added `CHANGELOG` * more tidying up * streamlined `import`s * removed `Recomputable` from `Relation.Nullary` * fixed multiple definitions in `Relation.Unary` * reorder `CHANGELOG` entries after merge * `contradiciton` via `weak-contradiction` * irrefutable `with` * use `of` * only use *irrelevant* `⊥-elim-irr` * tightened `import`s * removed `irr-contradiction` * inspired by #2329 * conjecture: all uses of `contradiction` can be made weak * second thoughts: reverted last round of chnages * lazier pattern analysis cf. #2055 * dependencies: uncoupled from `Recomputable` * moved `⊥` and `¬ A` properties to this one place * removed `contradictionᵒ` and rephrased everything in terms of `weak-contradiction` * knock-on consequences; simplified `import`s * narrow `import`s * narrow `import`s; irrefutable `with` * narrow `import`s; `CHANGELOG` * narrow `import`s * response to review comments * irrelevance of `recompute` * knock-on, plus proof of `UIP` from #2149 * knock-ons from renaming * knock-on from renaming * pushed proof `recompute-constant` to `Recomputable` * Refactor `List.Membership.*` and `List.Relation.Unary.Any` (#2324) * `contradiction` against `⊥-elim` * tightened `import`s * added two operations `∃∈` and `∀∈` * added to `CHANGELOG` * knock-on for the `Propositional` case * refactor `lose∘find` and `find∘lose` in terms of new lemmas `∃∈-Any∘find` and `find∘∃∈-Any` * `CHANGELOG` * reorder * knock-on viscosity * knock-on viscosity; plus refactoring of `×↔` for intelligibility * knock-on viscosity * tightened `import`s * misc. import and other tweaks * misc. import and other tweaks * misc. import and other tweaks * removed spurious module name * better definition of `find` * make intermediate terms explicit in proof of `to∘from` * tweaks * Update Setoid.agda Remove redundant import of `index` from `Any` * Update Setoid.agda Removed more redundant `import`ed operations * Update Properties.agda Another redundant `import` * Update Properties.agda Another redundant `import`ed operation * `with` into `let` * `with` into `let` * `with` into `let` * `with` into `let` * indentation * fix `universal-U` * added `map-cong` * deprecate `map-compose` in favour of `map-∘` * explicit `let` in statement of `find∘map` * knock-on viscosity: hide `map-cong` * use of `Product.map₁` * revert use of `Product.map₁` * inlined lemmas! * alpha conversion and further inlining! * correctted use of `Product.map₂` * added `syntax` declarations for the new combinators * remove`⊥-elim` * reordered `CHANGELOG` * revise combinator names * tighten `import`s * tighten `import`s * fixed merge conflict bug * removed new syntax * knock-on * Port two Endomorphism submodules over to new Function hierarchy (#2342) * port over two modules * and add to CHANGELOG * fix whitespace * fix warning: it was pointing to a record that did not exist. * fix things as per Matthew's review - though this remains a breaking change. * take care of comments from James. * adjust CHANGELOG for what will be implemented shortly * Revert "take care of comments from James." This reverts commit 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385. * Revert "fix things as per Matthew's review - though this remains a breaking change." This reverts commit d1cae72dcb3b44d4ba3c7290f3535544be32ab1e. * Revert "fix whitespace" This reverts commit 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2. * Revert "port over two modules" This reverts commit 6619f114346e86ead3cf62b1170ab23d31056b48. * rename these * fix tiny merge issue * get deprecations right (remove where not needed, make more global where needed) * style guide - missing blank lines * fix a bad merge * fixed deprecations * fix #2394 * minor tweaks --------- Co-authored-by: James McKinna * Add `IsIdempotentMonoid` and `IsCommutativeBand` to `Algebra.Structures` (#2402) * fix #2138 * fixed `Structures`; added `Bundles` * added fields; plus redefined `IsSemilattice` and `IsBoundedSemilattice` as aliases * `fix-whitespace` * reexported `comm` * fixed `Lattice.Bundles` * knock-on * added text about redefinition of `Is(Bounded)Semilattice` * add manifest fields to `IsIdempotentSemiring` * final missing `Bundles` * `CHANGELOG` * [ new ] Word8, Bytestring, Bytestring builder (#2376) * [ admin ] deprecate Word -> Word64 * [ new ] a type of bytes * [ new ] Bytestrings and builders * [ test ] for bytestrings, builders, word conversion, show, etc. * [ ci ] bump ghc & cabal numbers * [ fix ] actually set the bits ya weapon * [ ci ] bump options to match makefile * [ ci ] more heap * [ more ] add hexadecimal show functions too * Update LICENSE (#2409) * Update LICENSE year * Remove extraneous 'i' --------- Co-authored-by: Lex van der Stoep * Remove (almost!) all external use of `_≤″_` beyond `Data.Nat.*` (#2262) * additional proofs and patterns in `Data.Nat.Properties` * added two projections; refactored `pad*` operations * `CHANGELOG` * removed one more use * removed final uses of `<″-offset` outside `Data.Nat.Base|Properties` * rename `≤-proof` to `m≤n⇒∃[o]m+o≡n` * removed new pattern synonyms * interim commit: deprecate everything! * add guarded monus; make arguments more irrelevant * fixed up `CHANGELOG` * propagate use of irrelevance * tidy up deprecations; reinstate `s<″s⁻¹` for `Data.Fin.Properties` * tightened up the deprecation story * paragraph on use of `pattern` synonyms * removed `import` * Update CHANGELOG.md Fix refs to Algebra.Definitions.RawMagma * Update Base.agda Fix refs. to Algebra.Definitions.RawMagma * inlined guarded monus definition in property * remove comment about guarded monus * Refactor `Data.Sum.{to|from}Dec` via move+deprecate in `Relation.Nullary.Decidable.Core` (#2405) * fixes #2059 on the model of #2336 * fixed `import` dependencies * simplified `import` dependencies * final tweak * `CHANGELOG` * Implement move-via-deprecate of `decToMaybe` as per #2330 (#2336) * Make the main home of `decToMaybe` be `Relation.Nullary.Decidable.Core`, but deprecate the one in `Data.Maybe.Base` instead of removing it entirely. Fix the library accordingly. Note that this forces `Relation.Nullary.Decidable.Core` to use `Agda.Builtin.Maybe` to avoid a cyclic import. This can be fixed once the deprecation is done. * Update src/Relation/Nullary/Decidable/Core.agda Good idea. Co-authored-by: G. Allais * simplified the deprecation * `CHANGELOG` * narrowed import too far * tweak a couple of the solvers for consistency, as per suggestions. * chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe` * Revert "chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`" This reverts commit 256a50589dacab913c69f4db5b4570b46cf440d7. * `fix-whitespace` * simplify `import`s * make consistent with `Idempotent` case * tidy up * instead of an alias, open public so that Agda knows these really are the same. This is a better deprecation strategy. * rename(provisional)+deprecate * knock-on * knock-on: refactor via `dec⇒maybe` * deprecation via delegation * fix `CHANGELOG` --------- Co-authored-by: G. Allais Co-authored-by: James McKinna Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * fixes #2411 (#2413) * fixes #2411 * now via local -defined auxiliaries * Tidy up CHANGELOG in preparation for v2.1 release candidate (#2412) * Tidy up CHANGELOG in preparation for v2.1 release candidate * Fixed WHITESPACE * Fixed James' feedback and improved alphabetical order * [v2.1-rc1] fixes #2400: use explicit quantification instead (#2429) * fixes #2400: use explicit quantification * fix knock-ons * Revert "Improve `Data.List.Base` (fix #2359; deprecate use of `with` #2123) (#2365)" (#2423) This reverts commit 438f9ed4c30751be35718297bbe0c8ec7d3fb669. Specifically, it restores `with`-based definitions of the `Decidable`-definable functions on `List`s, incl. `filter` Fixes #2415 * implicit to explicit in `liftRel` (#2433) * fix changelog (#2435) couple fixes for changelog rendering * Export missing IsDecEquivalence instance for Quantity from Reflection.AST.Instances * Add missing `showQuantity` function to Reflection.AST.Show * Compatibility with Agda PR #7322: add quantity to reflected syntax of constructor * Bump CI for experimental to latest Agda master * Final admin changes * Added v2.1.1 CHANGELOG entry * Fix #2462 by removing duplicate infix definition * Updated remaining documentation for v2.1.1 release * Update CHANGELOG.md typo * Update CHANGELOG.md * Update installation-guide.md * Update src/Reflection/AST/Definition.agda Fix typo * Update CITATION.cff bring the date forward to today --------- Co-authored-by: Saransh Chopra Co-authored-by: Maximilien Tirard Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Co-authored-by: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com> Co-authored-by: Alex Rice Co-authored-by: Guilherme Silva Co-authored-by: Jacques Carette Co-authored-by: Ambroise Co-authored-by: Andreas Abel Co-authored-by: Nathan van Doorn Co-authored-by: Akshobhya K M Co-authored-by: shuhung Co-authored-by: fredins Co-authored-by: Nils Anders Danielsson Co-authored-by: Ioannis Markakis <70938217+jmarkakis@users.noreply.github.com> Co-authored-by: G. Allais Co-authored-by: Amélia Co-authored-by: James Wood Co-authored-by: Jesin Co-authored-by: jamesmckinna Co-authored-by: Guilherme Co-authored-by: Piotr Paradziński Co-authored-by: lemastero Co-authored-by: Gan Shen Co-authored-by: Gan Shen Co-authored-by: Uncle Betty <3210857+uncle-betty@users.noreply.github.com> Co-authored-by: Chris Co-authored-by: Alba Mendez Co-authored-by: Naïm Favier Co-authored-by: Orestis Melkonian Co-authored-by: Lex van der Stoep Co-authored-by: Lex van der Stoep Co-authored-by: Jesper Cockx

Generalise Data.Product.Relation.Binary.Pointwise.NonDependent to REL #906

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Generalise `Data.Product.Relation.Binary.Pointwise.NonDependent` to REL #906