André Videla
André Videla
> there are no copatterns in Idris2 right now? that's right, we still need to implement copatterns
yeah that should probably not be allowed
So I've been playing with this for a bit in the past few days and my conclusion is that interface elaboration is subtly broken in very annoying ways. Like you...
> constraints also need to remain fields in order to be available at runtime. That is not the case! Parameters are available at runtime as long as they are not...
It took me a second to realise why my statement was wrong, but it's because the _type constructor_ has the unrestricted multiplicity not the data-constructor.
The string is never used at runtime edit: I was on the train so that's all I had time to write. To elaborate, the string tag is only there to...
This is an example of "uninformative matching" right?
Yeah this is expected behaviour. The error message should be better. In this case we can detect the problem as we are defining `op` since the syntax extension is already...
I think the gambit backend should be treated as a third party backend rather than live within the idris repo. Maybe we could extract it to idris-community ?
> PPCSnowLeopardPorts Just curious: Are you running Snow Leopard on PowerPC hardware? Real questions: - I see mentions of MacPort, are you building from source, pack, homebrew, or from macport?...