Edwin Brady

We should be supporting multiple back ends, and dealing with multiple FFIs, though I'm no longer convinced that the type based approach from Idris 1 is the best way especially...

Ah, you mean for the Idris implementation in Blodwen, I see. This is going to get confusing ;). I think the simplest way to go here would be to find...

Hi, sorry to keep you. I think this is fine especially if it helps keep the JVM build going, as long as the default in this repo remains the C...

I'm trying something a bit different in the core for representation of metavariables, which I'll make public soonish, and while I'm at it I'm taking the chance to fix some...

At least at compile time, it's almost certainly down to the `fromInteger` which has to compute a proof that the Fin is within bounds. This is a compile time thing....

You can use :c at the REPL just like in Idris 1, as long as you have chez scheme installed. Nobody has implemented -o yet. There seems to be a...

So I've worked out what's going on - interestingly it's fast in Idris 1 because there it reduces everything to normal form, and it's slow in Idris 2 because it's...

It should be linear in N but I'm having trouble testing that experimentally because it erases things predictably in Idris 2 so I'm only really seeing the start up cost...

I've found that chicken takes quite a while to generate code from the scheme that Idris passes to it. It also generates code that is quite a bit slower than...

This is because at the REPL Idris doesn't know what type the 'Maybe' contains, since you haven't explicitly specified. It won't, in general, infer a type - in programs you...