Naïm Camille Favier
Naïm Camille Favier
Found a similar error on code that doesn't involve HITs: ```agda {-# OPTIONS --cubical #-} open import Cubical.Foundations.Prelude variable ℓ : Level A : Type ℓ lUnit : {x y...
Needs to be fixed in the paragraph just above as well.
This was done in https://github.com/plt-amy/1lab/pull/124
Maybe when multiple solutions exist, `C-c C-s` should prefer the "most constrained" one? i.e. first search for a solution forgetting all boundary conditions, then if it finds none add boundaries...
> Related: #4526. Some suggestions from that ticket that weren't implemented: > > * Add a `.agda-lib` file for the builtin modules. > > * Only allow a single, fixed...
That definitely sounds more sensible!
Bump? This would really be useful
> Is there be anything us developers will have to do in the future for example when releasing a new version of the library when there is a new version...
Right, `vector-hashtables` is broken in 22.05. I guess that's fine. Maybe the most flexible option is to also provide an overlay, just like the agda flake does, so that people...