agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
I’m working on a collection of proofs for submission to `Data.Fin.Properties`. I can phrase & prove via `cast` or via `subst Fin`. For my own use, I need the `subst`...
Some things that I keep meaning to add to the style-guide but never get around to: - naming disambiguation (see #1084) - sections and subsections (------------) - equation ordering `complex/compositional...
Follow up to #1063, which was partially addressed in #1585. Once the properties have been proved, there's an argument that we can remove the test suite added in #1585, though...
I believe that a bunch of "properties" of List's `All` should really be defined in the main `All` module, because they are just operations on heterogeneous lists. For example, the...
#1518 added a new golden testing framework to the standard library. It would be useful to extend the tests to cover more modules. However, at present, there is no documentation...
I'd like a function to turn a rational into its decimal expansion at a given precision. Perhaps with type `showDecimalAtPrecision : (precision : ℕ) → ℚ → String`, although maybe...
Now that it looks very likely we're going to use instance arguments for resolving `NonZero` proofs we should explore whether it's possible and/or desirable to automatically create derived instances to...
Algebra.Definitions.RawMagma defines ``` _∣_ : Rel A (a ⊔ ℓ) x ∣ y = ∃ λ q → (q ∙ x) ≈ y ``` (here I omit the upper index...
We have our left and rights switched round in `*-monoʳ-≤`, `*-monoʳ-≤-pos`. It would be kind of good if we had definitions for `Monotonic`/`LeftMonotonic`/`RightMonotonic` etc. in `Relation.Binary.Definitions` to help keep us...