agda pr 7349 #2441
Closed
agda pr 7349 #2441
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
* Eliminate many propositional equality imports * Fix merge conflict in Data.Bool.Properties Co-authored-by: G. Allais <[email protected]> --------- Co-authored-by: G. Allais <[email protected]>
To fix agda/agda#6654, we've decided that large indices will no longer be allowed by default. There is an infective flag `--large-indices` to bring them back, but none of the uses of large indices in the standard library were essential: to avoid complicated mutually-recursive PRs across repos, I adjusted the levels to check with `--no-large-indices` instead of adding the flag to the modules that used them.
* Simplify some `Relation.Binary` imports * Format * Better naming scheme * Fix tests * Merge issues
* Simplify leftover `Function` imports * `Function` -> `Function.Base` Co-authored-by: G. Allais <[email protected]> --------- Co-authored-by: G. Allais <[email protected]>
* Simplify more `Data.Product` import to `Data.Product.Base` * Missed an import
…#2019) * Simplify import of `Data.List.Relation.Binary.Pointwise` in agda-stdl * rectifications on Data.List.Relation.Binary.Pointwise import * rectifications on Data.List.Relation.Binary.Pointwise import * Delete weights-README.dot * Delete weight.png * Delete README.dot
* Simplify more `Data.Product` import to `Data.Product.Base` * Simplify more `Data.Product` import to `Data.Product.Base` * Indent
* Haskell CI (for GenerateEverything) and dependencies bumped to GHC 9.10.1 * CI: bump some versions, satisfy some shellcheck complaints
* 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
* 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.
* 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 <[email protected]>
* 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`
* `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 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 93e9e0f. * Revert "fix things as per Matthew's review - though this remains a breaking change." This reverts commit d1cae72. * Revert "fix whitespace" This reverts commit 81230ec. * Revert "port over two modules" This reverts commit 6619f11. * 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 <[email protected]>
…es` (#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`
* [ 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 year * Remove extraneous 'i' --------- Co-authored-by: Lex van der Stoep <[email protected]>
* 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
* 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 <[email protected]> * 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 256a505. * `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 <[email protected]> Co-authored-by: James McKinna <[email protected]> Co-authored-by: jamesmckinna <[email protected]>
* Tidy up CHANGELOG in preparation for v2.1 release candidate * Fixed WHITESPACE * Fixed James' feedback and improved alphabetical order
* fixes #2400: use explicit quantification * fix knock-ons
couple fixes for changelog rendering
|
Oops wrong repo. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
1\!≡1Nat._^_^-monoʳ-<and2^n>0by addingm^n>02^n>0Ring[clean version of pr opposite of aRing#1900] (opposite of aRing[clean version of pr #1900] #1910)"withCHANGELOGwithbindings for recursive calls/inductive hypothesesp->oCHANGELOG*.Categorical.*as deprecated modules (Restore deleted*.Categorical.*as deprecated modules #1946)inspect(Another attempt at deprecation ofinspect#1930)Setoid: definition and consequences #1953)Data.List.PropertiesDataandCodata(Fixities forDataandCodata#1985)System.Console.ANSI(Get rid of redundant deps inSystem.Console.ANSI#1994)take-[]anddrop-[]in CHANGELOG.md (Update CHANGELOG.md move 2 functions to section Data.List.Properties #1991)_↔̇_to the new Function hierarchy + more arrows for indexed sets (Migrate_↔̇_to the new Function hierarchy + more arrows for indexed sets #1982)Function,Data, andReflection(Fixities forFunction,Data, andReflection#1987)DataandCodata(Fixities forDataandCodata#1989)Relation.Binary.Construct.(Flip/Converse)(RenameRelation.Binary.Construct.(Flip/Converse)#1979)Relation.Binary.Construct.(Flip/Converse)#1979)System.Console.ANSI#1993 ] Simplifying the dependency graph ([ re #1993 ] Simplifying the dependency graph #1995)RelationandAlgebra(Fixities forRelationandAlgebra#1992)take-alltoData.List.Properties(added new functiontake-allto stdl #1983)take-drop-1andtake-one-moreadded to Data.List.Properties (New functionstake-drop-1andtake-one-moreadded to Data.List.Properties #1984)Functionimports (Cut downFunctionimports #2006)_buildcorrectly (gitignore_buildcorrectly #2010)Data.Productimports toData.Product.Base(SimplifyData.Productimports #2003)Data.Listimports toData.List.Base(SimplifyData.Listimports #2007)Relation.Binaryimports (Simplify someRelation.Binaryimports #2009)Data.Sumand leftoverData.Listimports #2011)Functionimports (Simplify leftoverFunctionimports #2012)Data.productimports (Simplify moreData.productimports #2014)Data.List.Relation.Binary.Pointwisein agda-stdl (Simplify import ofData.List.Relation.Binary.Pointwisein agda-stdl #2019)Data.Productimports toData.Product.Base(Simplify moreData.Productimports toData.Product.Base#2036)divides-refltoData.Nat.Divisibility.CoreRelation.Binaryimports (Simplify moreRelation.Binaryimports #2034)excluded-middle(Rename and deprecateexcluded-middle#2026)Stringimports (simplifiedStringimport in stdl #2016)Function.Definitionsto use strict inverses (Strict inverses #1156)take/drop/head -map-commuteadded to Data.List.Properties (functionstake/drop/head -map-commuteadded to stdl Data.List.Properties #1986)Vecimport (SimplifiedVecimport in stdl #2018)Data.Productsimplifications (MoreData.Productsimplifications #2039)Relation.Binaryimports (More simplifications forRelation.Binaryimports #2038)Data.Productimport simplifications (FinalData.Productimport simplifications #2052)xor(Add more properties forxor#2035)imports fromData.Bool.Base(removed redundantimports fromData.Bool.BaseinData.List.NonEmpty.Base#2062)Data.String(tidying upData.String#2061)Relation.Binarysimplifications (MoreRelation.Binarysimplifications #2053)drop-dropinData.List.Properties(Adddrop-dropinData.List.Properties#2043)push-function-into-iftake-drop-idandtake++drop(Renametake-drop-idandtake++drop#2069)find,findIndex, andfindIndicesforData.List(Addfind,findIndex, andfindIndicesforData.List#2042)Relation.Binarysimplifications (FinalRelation.Binarysimplifications #2068)CHANGELOG(spellcheckedCHANGELOG#2078)Reflection.AST(Refine imports inReflection.AST#2072)_∷ʳ_properties toData.Vec.Properties(Add some_∷ʳ_properties toData.Vec.Properties#2041)≡-setoidtoFunction.Indexed.Relation.Binary.Equality(Move≡-setoidtoFunction.Indexed.Relation.Binary.Equality#2047)WellFoundedproofs for transitive closure (WellFoundedproofs for transitive closure #2082)reverse,_++_andfromList(Add properties of vector selectors,Vec.reverse,Vec._++_andVec.fromList#2045)minor changessection in CHANGELOGsplitAt,takeanddropinData.List. (improve implementation of splitAt, take and drop. #2056)Fin n(a recursive view ofFin n#1923)Functionhierarchy everywhere. (Use new style function hierarchy everywhere. #1895)begin-irreflreasoning combinator (Addbegin-irreflreasoning combinator #1470)(Commutative)Semiring[supersedes Provide binomial theorem for commutative semiring #1287] (Proofs of the Binomial Theorem for(Commutative)Semiring[supersedes #1287] #1928)Relation.Nullarycode (ModerniseRelation.Nullarycode #2110)Algebra.Bundles.SemiringWithoutOneRelation.Binary.Definitions.Total#453: addedDenserelations andDenseLinearOrder(Ob #453: addedDenserelations andDenseLinearOrder#2111)Data.Rational.Unnormalised.*(Rectifies the negated equality symbol inData.Rational.Unnormalised.*#2118)ListandVec(Sync insert, remove, and update functionalities forListandVec#2049)Relation.Binary.Bundles.Preorder._∼_(De-symmetrisingRelation.Binary.Bundles.Preorder._∼_#2099)Data.Nat.Base._≤″_(RedefinesData.Nat.Base._≤″_#1948)iterateandreplicateforListandVec(SynciterateandreplicateforListandVec#2051)yto implicit inInduction.WellFounded.WfRec(Changes explicit argumentyto implicit inInduction.WellFounded.WfRec#2084)Relation.Binary.Properties.HeytingAlgebrain the wrong place #2130] MovingProperties.HeytingAlgebrafromRelation.BinarytoRelation.Binary.Lattice([fixes #2130] MovingProperties.HeytingAlgebrafromRelation.BinarytoRelation.Binary.Lattice#2131)inspect, ctd. #2127] Fixes Another attempt at deprecation ofinspect#1930importbug ([fixes #2127] Fixes #1930importbug #2128)_≮_and_≰_to bundles in the binary relation hierarchy. #1214] Add negated ordering relation symbols systematically toRelation.Binary.*([fixes #1214] Add negated ordering relation symbols systematically toRelation.Binary.*#2095)_<_onNat, plus consequences (Refactoring (inversion) properties of_<_onNat, plus consequences #2000)Algebra.Ordered(RemoveAlgebra.Ordered#2133)Reflection.TCM(Update blockOnMeta → blockTC #1972)IsStrictTotalOrder(Change definition ofIsStrictTotalOrder#2137)_⟨$⟩_operator for Function bundle #2144)Reasoning.Syntaxmodule (Make reasoning modular by adding newReasoning.Syntaxmodule #2152)Function.BundlesL185, L195 #2154 (Fixes typos identified in #2154 #2158)returnfromIO.Primitive#2124 as regardscase_return_of_(Tackles #2124 as regards renamingcase_return_of_#2157)_∷=_and_─_fromData.List.Membership.Setoid#2153 ] Properly re-export specialised combinators ([ fix #2153 ] Properly re-export specialised combinators #2161)LeftInversewith (Split)Surjection(ConnectLeftInversewith (Split)Surjection#2054)<-transˡ([fixes #2171] #2173)README/README.*#2175] Documentation misc. typos etc. for RC1 ([fixes #2175] Documentation misc. typos etc. for RC1 #2183)•: in•-cong : Congruent₂ _•_inAlgebra.Consequences.Setoid#2178] regularise and specify/systematise, the conventions for symbol usage ([fixes #2178] regularise and specify/systematise, the conventions for symbol usage #2185)T?toRelation.Nullary.Decidable.Core(MoveT?toRelation.Nullary.Decidable.Core#2189)doc/directory ([ fix #1743 ] move README todoc/directory #2184)installation-guide,README.agda,README.md... (documentation: fix link toinstallation-guide,README.agda,README.md... #2197)v1.6perhaps? (Easy deprecation inRelation.Unary.Consequences; leftover fromv1.6perhaps? #2203)Function.Consequences.Setoid(AddFunction.Consequences.Setoid#2191)Relation.Binary.PropositionalEquality.isPropositional(DeprecatingRelation.Binary.PropositionalEquality.isPropositional#2205)IrreducibleandRough; refactoring ofPrimeandCompositecf. (re-)Definition ofPrime(andIrreducible) inData.Nat.Primality#2180 (definition ofIrreducibleandRough; refactoring ofPrimeandCompositecf. #2180 #2181)Algebra.Consequences.*to reflectstyle-guideconventions ([fixes #2168] Change names inAlgebra.Consequences.*to reflectstyle-guideconventions #2206)Semilatticeoperation name #2166 by fixing names inIsSemilattice(Fixes #2166 by fixing names inIsSemilattice#2211)Category.*(remove final references toCategory.*#2214)zeroinIsRing#2195 by removing redundant zero from IsRing (Fix #2195 by removing redundant zero from IsRing #2209)Data.Nat.DivisibilityandData.Nat.DivMod([fixes #1711] RefactoringData.Nat.DivisibilityandData.Nat.DivMod#2182)standard-library.agda-lib? #2232] ([fixes #2232] #2233)maptoData.String.Base(AddmaptoData.String.Base#2208)Data.Nat.Divisibilityuse vertical bar rather than dvisibility operator in their names #2237 (fixes issue #2237 #2238)README.md#2234 (UpdateREADME#2241)HACKING(UpdateHACKING#2242)less-than-or-equalbeyondData.Nat.*(Remove all external use ofless-than-or-equalbeyondData.Nat.*#2256)Relation.Nullary.Decidable.Core.isYes#2271)style-guide(additions tostyle-guide#2270)_× x(lemmas about semiring structure induced by_× x#2272)Data.Natfixing Standardise names for qualified module imports #2280 (Qualified import ofData.Natfixing #2280 #2281)README.Data.Fin.Substitution.UntypedLambda#2279)Data.Product.Basefixing Standardise names for qualified module imports #2280 (Qualified import ofData.Product.Basefixing #2280 #2284)Propertiesmodules (Qualified import ofPropertiesmodules fixing #2280 #2283)READMEmodules #1380 (README.Data.*manual fix for #1380 #2285)sized-typeserror in orphan module (Fixsized-typeserror inREADME.Data.Tree.Binary#2295)PropositionalEqualityetc. fixing Standardise names for qualified module imports #2280 (Qualified import ofPropositionalEqualityetc. fixing #2280 #2293)Data.Sum.Basefixing Standardise names for qualified module imports #2280 (Qualified import ofData.Sum.Basefixing #2280 #2290)Data.Integer.Divisibilityfixing Standardise names for qualified module imports #2280 (Qualified imports inData.Integer.Divisibilityfixing #2280 #2294)-Reasoningmodule imports (Style guide: guideline for-Reasoningmodule imports cf #2282 #2309)renamingon qualified import cf. Qualified imports inData.Integer.Divisibilityfixing #2280 #2294 (Style guide: avoidrenamingon qualified import cf. #2294 #2308)mkRawMonadandmkRawApplicativeuniverse-polymorphic (makemkRawMonadandmkRawApplicativeuniverse-polymorphic #2314)READMEimports Standardise names for qualified module imports #2280 (Tidy upREADMEimports #2280 #2313)InitialandTerminalalgebras (Add unique morphisms from/toInitialandTerminalalgebras #2296)Accessible elements of)WellFoundedrelations ('No infinite descent' for (Accessible elements of)WellFoundedrelations #2126)RawQuasigroup) toIsGroup(Add new operations (cf.RawQuasigroup) toIsGroup#2251)Data.List.Relation.Binary.BagAndSetEquality(RefactorData.List.Relation.Binary.BagAndSetEquality#2321)Data.List.Relation.Unary.Any.Properties: remove dependency onList.Properties(SimplifyData.List.Relation.Unary.Any.Properties: remove dependency onList.Properties#2323)Data.Integer.Divisibility.Signed(RefactorData.Integer.Divisibility.Signed#2307)Induction.RecStructwithRelation.Unary.PredicateTransformer.PT(Predicate transformers: ReconcilingInduction.RecStructwithRelation.Unary.PredicateTransformer.PT#2140).Coremodule (Move pointwise equality to.Coremodule #2335)Algebra.Bundles.SuccessorSetand related records #2273] AddSuccessorSetand associated boilerplate ([fixes #2273] AddSuccessorSetand associated boilerplate #2277)Relation.Binary.Definitions.DecidableEquality(Systematise use ofRelation.Binary.Definitions.DecidableEquality#2354)Data.List.Base.mapMaybe(List of sub-optimal definitions inData.List.Base#2359; deprecate use ofwithRefactoring uses ofwith#2123) (ImproveData.List.Base.mapMaybe(#2359; deprecate use ofwith#2123) #2361)Data.List.Base.unfold(List of sub-optimal definitions inData.List.Base#2359; deprecate use ofwithRefactoring uses ofwith#2123) (ImproveData.List.Base.unfold(#2359; deprecate use ofwith#2123) #2364)zerofield inAlgebra.Structures.Biased.IsRing*? #2253 ([fix #2253] DeprecateAlgebra.Structures.Biased.IsRing*#2357)Data.Nat.Solverfrom a number of places (Remove uses ofData.Nat.Solverfrom a number of places #2337)Data.List.Base(fix List of sub-optimal definitions inData.List.Base#2359; deprecate use ofwithRefactoring uses ofwith#2123) (ImproveData.List.Base(fix #2359; deprecate use ofwith#2123) #2365)withare not really needed (A number ofwithare not really needed #2363)_>>_forIO.Primitive.Core(Add_>>_forIO.Primitive.Core#2374)isEquivalence(RefactorFunction.Relation.Binary.Setoid.Equalityto lift outisEquivalence#2382)Data.List.Base.reverseis self adjoint wrtData.List.Relation.Binary.Subset.Setoid._⊆_(Data.List.Base.reverseis self adjoint wrtData.List.Relation.Binary.Subset.Setoid._⊆_#2378)mapfor⊆as Subset #2375 (fixes #2375 #2377)Data.List.Relation.Binary.Sublist.Setoidcategorical properties (AddData.List.Relation.Binary.Sublist.Setoidcategorical properties #2385)Algebra(PointwiseAlgebra#2381)Data.List.Base.scan*and their properties (RefactorData.List.Base.scan*and their properties #2395)variableblock indentation style #2390 (style-guiderule for initialprivateblock in modules #2392)Setoid-basedMonoidon(List, [], _++_)(Add theSetoid-basedMonoidon(List, [], _++_)#2393)Data.Product.Relation.Binary.Pointwise.NonDependentto REL #906 (GeneraliseData.Product.Relation.Binary.Pointwise.NonDependent.Pointwise#2401)catMaybes/mapMaybe(More list properties aboutcatMaybes/mapMaybe#2389)Data.List.Base(fix List of sub-optimal definitions inData.List.Base#2359; deprecate use of with Refactoring uses ofwith#2123) (ImproveData.List.Base(fix #2359; deprecate use of with #2123) #2366)Relation.Nullary.Recomputableplus consequences (AddsRelation.Nullary.Recomputableplus consequences #2243)List.Membership.*andList.Relation.Unary.Any(RefactorList.Membership.*andList.Relation.Unary.Any#2324)IsIdempotentMonoidandIsCommutativeBandtoAlgebra.Structures(AddIsIdempotentMonoidandIsCommutativeBandtoAlgebra.Structures#2402)_≤″_beyondData.Nat.*(Remove (almost!) all external use of_≤″_beyondData.Nat.*#2262)Data.Sum.{to|from}Decvia move+deprecate inRelation.Nullary.Decidable.Core(RefactorData.Sum.{to|from}Decvia move+deprecate inRelation.Nullary.Decidable.Core#2405)decToMaybeas per movedecToMaybefromData.Maybe.BasetoData.Maybe#2330 (Implement move-via-deprecate ofdecToMaybeas per #2330 #2336)tail∘initsandtail∘tails#2411 (fixes #2411 #2413)Data.List.Base(fix List of sub-optimal definitions inData.List.Base#2359; deprecate use ofwithRefactoring uses ofwith#2123) (ImproveData.List.Base(fix #2359; deprecate use ofwith#2123) #2365)" (Fix v2.1-rc1 by reverting (some) changes toData.List.*#2423)liftRel([v2.1-rc1] Change quantification from implicit to explicit inAlgebra.Construct.Pointwise.liftRel#2433)showQuantityfunction to Reflection.AST.Show