agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
The usual convention in math is that the shapes of inf/sup-operators are chosen consistent with the shape of the comparison relation, with typical flavors being: - rectangular - round -...
I was expecting that `DecTotalOrder` gives me operations to compute the minimum and maximum, but could not find them. (These are declared in the `Lattice` hierarchy.) I think it would...
The results in `Algebra.Operations.CommutativeMonoid` would really benefit from being proved over a suitable `Foldable` structure rather than individually for `List`/`Vec`/`Vector` etc. See https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Foldable.html Perhaps someone whose familiar with it, could...
Should we add an `Algebra.Structures.Literals` module declaring a `Number` instance for any `SemiringWithoutAnnihilatingZero` interpreting `n` as `1 + ... + 1`?
For ``P : Pred A _, f : A → A``, what is the standard library type definition for ``{x : A} → P x → P (f x)`` ?...
The solver defines its own version of exponentiation in `Algebra.Operations.Ring` that differs from that in `Data.Nat.Base`. This means that the solver does not work for equations involving exponentiation in `Data.Nat.Base`....
As pointed out by @jamesmckinna when trying to update PFLA to use v1.7 of the library (analysis below is his), currently you can't use `¬_` from `Relation.Nullary` and `∃[ A...
Implication, like `xor` is derivable. We go through various hoops to derive `xor` generically for any boolean algebra below: https://github.com/agda/agda-stdlib/blob/69c808fa1491eaff678cb9e29961e6068ef9f1ad/src/Algebra/Lattice/Properties/BooleanAlgebra.agda#L246-L249 I wonder if there's a middle ground.
In #1123 we are talking about a breaking change to a module that was just released. Hence the question: should we add a user warning to new modules telling people...
Currently the combinators use `≈` instead of `≃`