agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
Matthew wrote > The discussion for how this stage of the changes should be laid out should > really be continued in an issue on Github. If you'd like to...
It would be a great to have matrices in the standard library. In https://github.com/agda/agda-stdlib/pull/1525 I opened a small PR with a very simple implementation of `Data.Matrix`. Thanks to a valuable...
lib-1.7 has a general notion AlmostLeft(Right)Cancellative, and it is used in `*-cancelˡ-nonZero` in `IsCancellativeCommutativeSemiring`. On the other hand `Nat.Properties` has the definitions of kind. ``` *-cancelʳ-≡ : ∀ m n...
Relation.Binary.Core has ` _Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _` And I introduce ```agda Respects₂gen :...
In `Data.Integer.Properties`, ```agda pos-distrib-* : ∀ x y → (+ x) * (+ y) ≡ + (x ℕ* y) ``` is the symmetric of the *not yet existing* function ```agda...
In [`Data.List.Properties`](https://agda.github.io/agda-stdlib/Data.List.Properties.html#2896) we use `map-compose` whereas in [`Data.Vec.Properties`](https://agda.github.io/agda-stdlib/Data.Vec.Properties.html#5621) we use `map-∘`.
We have currently ```agda data Delay {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where ``` but I think swapping `A` and `i` would be more natural;...
In `Data.List.Properties` we use * `map-id₂ : All (λ x → f x ≡ x) xs → map f xs ≡ xs` * `map-cong₂ : All (λ x → f...
Currently the definition is: ```agda _⋆C_ : ∀ {x s p} → Container s p → Set x → Container (s ⊔ x) p C ⋆C X = const X...
it is interesting to see that there is no induced products and sums of setoids in this library yet. do I just overlook it or is it indeed the case.
