Nils Anders Danielsson
Nils Anders Danielsson
> I do not think it is useful to build the coding styles of the current libraries into the language itself. We could go with your approach, but in that...
I think one should also ensure that no variable is used twice in the solution.
> What if the 'proper' long normal form was `λ {record {l = l; r = r} → c l r}` instead ? Then everything is much more clearly linear....
> I'm using pattern-matching lambda, as in > > ```agda > postulate D : Set > record XX : Set where > constructor c > field > l : D...
I prefer bag/set equivalence to bag/set equality. (I used to refer to the relations as equalities, but Fritz Henglein convinced me that the term equivalence is better.)
I don't know why this was not labelled with `false`. It is easy to flesh out the example into one that type-checks with `--erased-cubical --safe`.
> Proposal: disallow `--syntax-based-termination` when `--cubical` and `--safe` are on. (Or at least warn.) The new type-based termination checker has not been released yet. I don't think we should "force"...
> The OP could probably be fixed by declaring `MyList : ++Set -> Set` after merging: > > - #6385 This does not quite work. I opened a new issue...
Perhaps one could make Agda keep track of whether `-Werror` would have made Agda reject the code. Then code that would not have been rejected could be made compatible with...
We have discussed optionally disallowing the unit type with η-equality, so a translation that does not rely on that type might be preferable.