Nils Anders Danielsson
Nils Anders Danielsson
It is easy for me to work around the problem (at least this particular instance of it).
Here is a self-contained piece of code: ```agda open import Agda.Builtin.Bool open import Agda.Builtin.Equality open import Agda.Builtin.List open import Agda.Builtin.Reflection open import Agda.Builtin.Unit cong : {A B : Set} {x...
> In particular because it just bails (instead of blocking) when encountering a meta You asked for short code, and I seem to have removed too much: the code from...
Can we draw any conclusions from this? * Should Agda schedule things in a different way? * Is there a way to write macros in such a way that they...
@jespercockx, what action do you think should be taken, if any?
> Practically, the most feasible way to implement this would be by having an erasure annotation for each `def` and `con` in the internal syntax. Two `def`s with the same...
> Another option would be to not allow erased modules in general Did you mean erased import statements? Erased modules are already implemented, and the following code works: ```agda {-#...
> * Inference to be enabled by default for backwards-compatibility Note that the current inference does not seem to affect types. The following code is at least rejected: ```agda {-#...
I'm in favour of more shadowing (#3801), but I think it sounds like a bad idea to change the scoping rules for `let` but not `where`.
> As I mentioned on Zulip, one needs to check if conditions listed in the license of every package Agda uses are met before releasing an official binary. The cabal-plan...