agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
These are some lemmata we needed in our project [Vatras](https://github.com/VariantSync/Vatras) for reasoning on non-empty lists. It seemed these lemmata could be generally useful to other people as well. -- _PR...
Introduce a new module for equational reasoning in semigroups, providing utilities for associativity reasoning and operations.
I've been sniped by https://github.com/agda/agda-stdlib/pull/2723. This is a preparatory PR for the full proof that sorting two lists that are permutations of each other result in equal lists.
- Replace `Data.List.Base as List` and `Data.List.Properties as List` with shorter `L` aliases throughout the module for better readable proof - Add new utility lemma `toList-injective` that proves vector equality...
Fix #2547 for `Relation.Binary.Definitions.*`: - [x] `Transitive` - [x] `Antisym` - [x] `Antisymmetric` - [x] `CHANGELOG`
Besides the sorted and permutation peroperties, we also proved a congruence between permutation relation and pointwise relation on lists. And then we prove permuation relation is decidable.
Currently, we have in [`Data.Fin.Properties`](https://github.com/agda/agda-stdlib/blob/dc7ef5fa3aac5aa73631c6c644f3b5b12f30d56f/src/Data/Fin/Properties.agda#L1031-L1035) ```agda cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} → Injective _≡_ _≡_ f → Injective...
This PR adds proofs that projections from the product type are structure preserving maps (morphisms) from the direct product construction. This not complete whatsoever, but at least it gives an...
Alternative definition, as described in #2311, and towards open problems arising from #2723 and #2725 NB.: * UPDATED: I've previously misattributed this to Ralf Hinze, but credit properly belongs to...
The function `Data.Word64.Show.showHexa` blows up when I try to normalize for example `showHexa (fromℕ 0xdeadcafe)` in Emacs. The reason for this presumably is that it uses `Data.Nat.Show.showInBase`, which in turn...
