Jacques Carette
Jacques Carette
`Language.Drasil.Code.Imperative.GOOL.LanguageRenderer` contains stuff with a comment " Common syntax for several renderers." which is quite misleading: it is common indeed, but it isn't "syntax" per se, but rather default configuration...
`commonIdea` and `commonIdeaDict` should check if the list they are given is empty and, if so, complain. `mkIdea` should be used instead. There are quite a few abuses of this...
As per #3372 , @bmaclach comments that there exists GOOL tests - but these are not part of the Drasil test suite right now. This should be fixed. And likely...
> Fascinating how these next proofs are essentially the `cancel` and `elim` (left and right) combinators in `Categories.Morphism.Reasoning` ! _Originally posted by @JacquesCarette in https://github.com/agda/agda-stdlib/pull/2251#discussion_r1469634123_ The point would be that...
Looks like the CI uses GHC 8.10.7 (see `.github/workflows/ci-ubuntu.yml`) and cabal 3.6.2.0. Agda itself now seems to use stack and GHC 9.8.1. That's a very large gap!
The "improved" implementation of PR #2056 still is flawed. For ease of comparison, it is ```agda splitAt : ∀ m {n} (xs : Vec A (m + n)) → ∃₂...
I would love to see a `DESIGN.org` file documenting all the design choices (beyond cubical) where cubical-categories differs from agda-categories (any why). For example, I agree that `CommutativeSquare` is better...
(bottom up, i.e. from files with fewest dependencies first) - Concepts - why is `projectileTitle` defined here? It's not really a 'Concept' in the same sense as the others. -...
Closes #833 . The names, of course, are up for debate! (And, now that I think of it, I should probably add a property or two of them in this...
Make the main home of `decToMaybe` be `Relation.Nullary.Decidable.Core`, but deprecate the one in `Data.Maybe.Base` instead of removing it entirely. Fix the library accordingly. Note that this forces `Relation.Nullary.Decidable.Core` to use...