Steve Dunham

Given: ```idris parameters (n : Nat) data Bad : Type where ABad : Bad ``` I get: ``` :t ABad Main.ABad : (n : Nat) -> Bad n ``` Is...

Yeah, I just wasn't sure if `parameters` were supposed to apply to constructors. I think I've got a good mental model now. They're added to constructors and functions and are...

I've been setting `CPATH="/opt/homebrew/include"` to help Idris' Makefile find `gmp.h` installed by homebrew. This is done by the `install.sh` script in the snippet quoted above. This could be handled by...

I believe idris-lang/Idris2#3269 resolves this, can you double check @joelberkeley?

Ok, I’ve reproduced this with `nightly-240421` and verified that it no longer happens with `nightly-240428`.

I get this consistently in my client (OSX) the released version of 1.7.5 whenever I press "stop" on the server side. When I press "start" again on the server (OSX),...

Idris probably shouldn't use things with erased types as solutions for autos. It's interesting that the `TTC.idr` code suppresses those fields when `isUserName (fullname gdef) || cwName (fullname gdef)` but...

It looks like that change is trying to suppress the type information for metas. After they are solved, the definition is a `PMDef`, and I think they are indistinguishable from...

Yeah, it seems problematic to me that `Erased` converts to anything. I tried changing the that line and the previous one to `pure False` (along with sticking `True` in for...

I don't think the `5` example is consistent with the current behavior of `let`. Because of parsing for multiplicities, `let` will give a parse error for: ```idris let 5 :=...