Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* 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 <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* [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 <[email protected]>
* 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 <[email protected]>
* 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<ss
* Rename hasNonTrivialDivisor relation
* Updated CHANGELOG
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* [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 <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* 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 <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* [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<m`
* reverted change to `m/n≢0⇒n≤m`
* reverted breaking changes involving `NonZero` inference
* revised `CHANGELOG`
* restored deleted proof
* fix whitespace
* renaming: `DivMod.nonZeroDivisor`
* localised use of `≤-Reasoning`
* reverted export; removed anonymous module
* revert commit re `yes/no`
* renamed flipped equality
* tweaked comment
* added alias for `equality`
* [fixes #2232] (#2233)
* fixes #2232
* corrected major version number
* Add `map` to `Data.String.Base` (#2208)
* add map to Data.String
* Add test for Data.String map
* CHANGELOG.md add map to list of new functions in Data.String.Base
* precise import of Data.String to avoid conflict on map
* Fix import statements
---------
Co-authored-by: lemastero <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* Added Base to import
Co-authored-by: Nathan van Doorn <[email protected]>
* Added core to import
Co-authored-by: Nathan van Doorn <[email protected]>
* 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 <[email protected]>
Co-authored-by: Guilherme <[email protected]>
* 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 <[email protected]>
* [ 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 <[email protected]>
* 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 <[email protected]>
* make `mkRawMonad` and `mkRawApplicative` universe-polymorphic (#2314)
* make `mkRawMonad` and `mkRawApplicative` universe-polymorphic
* fix unresolved metas
---------
Co-authored-by: Gan Shen <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* '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 <[email protected]>
* [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 <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: Amélia <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: James Wood <[email protected]>
Co-authored-by: Andreas Abel <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* [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 <[email protected]>
* [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 <[email protected]>
* 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 <[email protected]>
* @gallais 's comments
* Update src/Data/List/Base.agda
Oops!
Co-authored-by: G. Allais <[email protected]>
---------
Co-authored-by: G. Allais <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* Update src/Data/Fin/Base.agda
layout for readability
Co-authored-by: G. Allais <[email protected]>
* Update src/Data/List/Fresh/Relation/Unary/All.agda
layout for readability
Co-authored-by: G. Allais <[email protected]>
---------
Co-authored-by: G. Allais <[email protected]>
* [ new ] ⁻¹-anti-homo-(// | \\) (#2349)
* [ new ] ¹-anti-homo‿-
* Update CHANGELOG.md
Co-authored-by: Nathan van Doorn <[email protected]>
* Update src/Algebra/Properties/Group.agda
Co-authored-by: jamesmckinna <[email protected]>
* Update CHANGELOG.md
Co-authored-by: jamesmckinna <[email protected]>
* [ more ] symmetric lemma
* [ new ] ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
---------
Co-authored-by: MatthewDaggitt <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
Co-authored-by: James McKinna <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* 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 <[email protected]>
* 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 <[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 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 <[email protected]>
Co-authored-by: James McKinna <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
* 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 <[email protected]>
Co-authored-by: Maximilien Tirard <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: Sofia El Boufi--Crouzet <[email protected]>
Co-authored-by: Alex Rice <[email protected]>
Co-authored-by: Guilherme Silva <[email protected]>
Co-authored-by: Jacques Carette <[email protected]>
Co-authored-by: Ambroise <[email protected]>
Co-authored-by: Andreas Abel <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: Akshobhya K M <[email protected]>
Co-authored-by: shuhung <[email protected]>
Co-authored-by: fredins <[email protected]>
Co-authored-by: Nils Anders Danielsson <[email protected]>
Co-authored-by: Ioannis Markakis <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: Amélia <[email protected]>
Co-authored-by: James Wood <[email protected]>
Co-authored-by: Jesin <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: Guilherme <[email protected]>
Co-authored-by: Piotr Paradziński <[email protected]>
Co-authored-by: lemastero <[email protected]>
Co-authored-by: Gan Shen <[email protected]>
Co-authored-by: Gan Shen <[email protected]>
Co-authored-by: Uncle Betty <[email protected]>
Co-authored-by: Chris <[email protected]>
Co-authored-by: Alba Mendez <[email protected]>
Co-authored-by: Naïm Favier <[email protected]>
Co-authored-by: Orestis Melkonian <[email protected]>
Co-authored-by: Lex van der Stoep <[email protected]>
Co-authored-by: Lex van der Stoep <[email protected]>
Co-authored-by: Jesper Cockx <[email protected]>- Loading branch information
34 people
authored
Sep 7, 2024
1 parent
ef9e3d6
commit 4144346