André Videla
André Videla
Looks like this has stalled because of styling changes. @locriacyber there is currently no style guide for Idris 2 and no plan to enforce one. Idris2 is still a young...
@locriacyber If I understand correctly @gallais 's intent you should write ``` preOption NoBanner = tuneSession { nobanner := True } ``` is that right @gallais ? My own feedback...
Thank you for pointing this out. The wiki is free to modify, would you (or someone else) be willing to perform the necessary updates?
It turns out we recently added a `Ur` constructor recently: https://github.com/idris-lang/Idris2/blob/main/libs/linear/Data/Linear/Notation.idr#L24 Maybe it should be moved to `prelude` or `base` so that we can use it for linear arrays
I've been thinking about that a lot lately and even when through partially implementing an alternative syntax for linear arguments. But I think we should hold off on this feature...
Ah that looks great actually!
To me it feels like the ideal solution would be: - removed the DecEq instance for doubles - Add a custom error message for trying to use decEq on Doubles...
sorry I was under the impression that decEq was the only way to get `0 = -0` but clearly you can just write it down and the compiler will happily...
I see! Thanks for explaining!
I just tried to install idris2 on my M1 laptop and I could not reproduce the issue. Everything worked fine, except for one thing. `gmp` couldn't be found so I...