Jacques Carette
Jacques Carette
All open issues that mention indexing, vectors, matrices, should be found and linked. This is part of the requirements analysis phase of this project.
So I was about to file an issue, based on the work at [Attributes and Chunks](https://github.com/JacquesCarette/Drasil/wiki/Attributes-and-Chunks) that went along the lines of "remove all `mkIdea` calls that use `Nothing` for...
See PR #43 for details. Judicious use of `open Setoid`? Also see if there are some `IndexedSetoid` lurking about.
One of the large sources of "funext" is this definition https://github.com/ualib/agda-algebras/blob/5a5687e95672d3648ffe4130a9a68afb4e0e9faf/UniversalAlgebra/Relations/Discrete.lagda#L77-L79 of `Op`. In theory, I like it a lot. That one can model arity by an arbitrary type, instead...
The global README leads me to believe that Pi combinators ≃ (Fin n ≃ Fin n) is really the desired end goal. [Though I'd prefer if the latter part was...
(Not quite sure who is still around!) For those who will be, please add your weekly summary if you will be @B-rando1 @Xinlu-Y @NoahCardoso @BilalM04 @balacij . I know @smiths...
This was started by @AKM11 (see #377 for some details, and code in `Language.Drasil.Misc`), but not quite finished. Definitely a good feature to have. As #377 what about a different...
Summary of routine changes: - use `.Base` for many modules instead of the "fat" top-level modules - don't use any deprecated modules under `Function` (`Function.Equivalence`, etc) and replace with `Function.Bundles`...
As per title.
While we should continue to define `System` in the examples, I think we should slowly stop using `System` in type signatures but instead move towards requiring getters for the needed...