André Videla

Results 112 comments of André Videla

[RFC] Library organisation

> I'm also willing to consider moving all libraries that aren't essential to the Idris 2 build into a new repository > In this case, we'd need a volunteer to...

Update INSTALL.md

Hi there, can you replace your link to discord with a summary of the situation? People on Github might not have access to discord, and it makes it easier to...

[ fix ] allow grouping pi with different types in type declaration

Are we sure we want this? wouldn't this add more confusion as to what `(,)` means? I'm also asking this because we could also dedicate this syntax to named positional...

[ fix ] allow grouping pi with different types in type declaration

I see the appeal, but I'm not quite sure if this is something we want just based on the grounds that we already have `(,)` overloading and `(a : Nat,...

Mention in the docs that `Foo =>` is `{auto _ : Foo} ->`

were you looking for this page? https://idris2.readthedocs.io/en/latest/updates/updates.html#auto-implicits-and-interfaces

Mention in the docs that `Foo =>` is `{auto _ : Foo} ->`

Indeed, the information is there but it seems everyone is missing it. Maybe we could create a page "idris2 desugarings" in here? https://idris2.readthedocs.io/en/latest/reference/index.html

Mention in the docs that `Foo =>` is `{auto _ : Foo} ->`

Indeed, maybe it could fit in the FAQ? https://idris2.readthedocs.io/en/latest/faq/faq.html?highlight=FAQ

Positivity checker accepts invalid datatype

Is this due to `Type : Type`?

Cannot compile prelude with latest Idris, file read error

I tried again today and here are my findings: It now fails at the `idris2-fromc` step, because `sed -i` isn't perfectly Multiplatform with Mac OS. I found this PR on...

Cannot compile prelude with latest Idris, file read error

Which commit were you using @ziman ?