Steve Dunham

I'm going to close this PR. We still have #2535 for the underlying issue, and I'll hold onto the tests. When new-core lands, we can see what it hasn't solved...

This error still occurs for me with Agda 2.6.3-b499d12. Repeatedly doing C-c C-r works, but C-c C-a says "Not implemented: The Agda synthesizer (Agsy) does not support literals yet". I'm...

For simplicity, we might drop the mention of the Racket Chez (and its build instructions). But since I added that, the instructions have simplified to: ```sh git clone [email protected]:racket/ChezScheme.git cd...

Also, homebrew is updated to include chez 10 for aarch64, so that should be the easiest path for mac users. (I don't use ports, so I don't know the situation...

I'd love to hear details when you get it sorted out. Homebrew is on chez 10 now (and ships idris2 against it). If it involves signal handling, chez bug 809...

> (Note that the shapes are 0-indexed, which is not typical. Is there an easy way to make them 1-indexed?) If you mean you'd like to have: ```idris ex1 :...

I think the underlying issue (possibly a bug) is that the case statement is being marked erased when it is pulled out to a top level function. I think stuff...

> For your 0 Ext_0_0_0 suggestion, what does that do? My understanding of this: The 0 marks the function as erased at runtime (quantity 0). That means the result of...

This issue also occurs when splitting on `Char`. It does not occur when splitting on `Bool` or `Nat`. ```idris 0 foo : (0 a : Char) -> Nat foo 'a'...

The case builder is dropping the second two cases in the following code: ```idris 0 foo : (0 a : Char) -> Nat foo 'a' = 1 foo 'c' =...