agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
Now that Agda 2.6.2 has been released, we don't need the `OPTIONS` pragmas everywhere, we can instead specify the default options in the `standard-library.agda` file. This should zap several hundred...
See the discussion https://github.com/agda/agda-stdlib/pull/1511#discussion_r650530794. I'd welcome any feedback from anyone else who has used it? https://github.com/agda/agda-stdlib/blob/358ad8bf673f0b292f5e5e86b50f0f6ec1d245cd/src/Relation/Binary/Indexed/Homogeneous/Core.agda#L32
`Data.Bool` imports a huge amount of stuff because it does ```agda open import Data.Bool.Properties public using (T?; _≟_; _≤?_; _
This PR extracts the new `begin-irrefl_` combinator proposed in #1385, and continues the conversation started in that PR. Summary so far: > @MatthewDaggitt > However I'm still reluctant to include...
We have Nary products but no Nary sums. It would be great to have some sort of general `injₙ i sum` syntax that would work with types involving multiple sums.
https://github.com/agda/agda-stdlib/blob/9076c9be0af3dfcdc78f8056cdf22d262cd4442e/src/Reflection/Show.agda#L74 Should print: - "." for irrelevant args - "@0" for erased arguments - etc.
In #1488 , I did not notice that `Data.Char` defines a bunch of relations which, in other parts, are done in separate sub-modules. In particular, I suggest that ```agda infix...
It's folklore that we can encode default implicit values in a DTT with instance arguments that may be explicitly applied. We should add this construct to the stdlib (I just...
Right now, we define function setoids as follows (taken from [Function.Equality](https://github.com/agda/agda-stdlib/blob/master/src/Function/Equality.agda#L79)): ```agda setoid : ∀ {f₁ f₂ t₁ t₂} (From : Setoid f₁ f₂) → IndexedSetoid (Setoid.Carrier From) t₁ t₂...
In the same way that we've avoided proving properties of `_⊔_` and `_⊓_` over and over again, we should avoid repeatedly proving properties about `|_|`. See the [four fundamental properties](https://en.wikipedia.org/wiki/Absolute_value#Real_numbers).