Jacques Carette
Jacques Carette
While looking at PR #2355 from @mildsunrise I noticed a ridiculous number of uses of `with`. These turn out to not be localized to `Data.List.Properties` but come from uses of...
Right now, `let` in Agda generates substitutions (as confirmed by Andreas [here](https://github.com/agda/agda/issues/5497) amongst other places). The [attempted fix](https://github.com/agda/agda/issues/3094) for this has stalled even though it is an [extremely old](https://github.com/agda/agda/issues/514) issue....
Since v1.2 (and before) were removed from v2.0, I'm removing v1.3 from v2.1. We probably could add in v1.4 as well, as there were very few things deprecated for that...
@jamesmckinna [mentions](https://github.com/agda/agda-stdlib/pull/2345#issuecomment-2047038663) that we ought to have a shopping list issue for 3.0. I think that using issues for that is sub-optimal. I'd prefer to either use the Wiki or...
Closes #2299 Needed to add some missing declarations in `Algebra.Morphism.Structures` to make it all go through.
`decToMaybe` drags in `Relation.Nullary.Reflects` and `Relation.Nullary.Decidable.Core` (which is a reasonable thing to do for its definition). But this seems like "overkill" for a `.Base` module as 'core' as for `Maybe`....
Note: I don't mean *mandate*, I mean *allow*. So the library sources would become a mixture of `.agda` and `.lagda` (which is a bit of a pain, I know.) Basically,...
We don't necessarily have the types we need to be able to represent discrete indices. We might not have the right "language of types" to let us describe such types...
Before doing a full design of indexable structures, we should have a list of what already exists in our examples.
We need to study the results of #3716 and #3717 to let us know what is needed in the design. This should result in some requirements with rationale, fit criteria...