agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
- [x] `ℚᵘ` is a `HeytingField` #1959 - [ ] `ℚ` is a `HeytingField` #2194
Probably WellFounded does not hold for
@jamesmckinna noticed a lack of lemmas relating renamings and substitutions, and I added some.
Currently http://agda.github.io/agda-stdlib/Text.Pretty.html suffers from various limitations: 1. Performance: [`__`](http://agda.github.io/agda-stdlib/Text.Pretty.html#2508) only filters the invalid results, it does not discard the dominated ones. This doesn't prevent combinatorial explosion (we've been experiencing issues...
For permutations on finite sets, as we have in `Data.Fin.Permutation`, it's possible to define their [parity](https://en.wikipedia.org/wiki/Parity_of_a_permutation). This isn't hard to define with what's in `Data.Fin.Permutation.Transposition.List`, something like ```agda parity :...
Adds versions of various inverses that compose in a strictly unital and associative way. i.e. Given `{A : Setoid} (f g h : Inverse A A)` we have ```agda2 (f...
So the issue title is a huge mouthful (and the text of this issue; -- sorry!), but the issue falls into two parts: * (general) ergonomics of 'pseudo' constructors/introduction forms...
Follow up from [#1727](https://github.com/agda/agda-stdlib/pull/1727) and https://github.com/agda/agda-stdlib/issues/1493
@gallais added the inspect idiom as a first class language construct in Agda 2.6.2. We should consider using it in the library to simplify our code, and possibly deprecating the...
Attempts to fix #1580. There's one small fly in the ointment and that's the following use in `Data.List.NonEmpty` https://github.com/agda/agda-stdlib/blob/5ac8015bccb973a02275ae8d1e6cf0550807ac49/src/Data/List/NonEmpty.agda#L68 where I get the dreaded `!= w` error below if I...