Ohad Kammar

Thanks! This problem does not necessarily have an infinite loop --- the proof terms are really big.

OK, so what's the best way to proceed?

I think this is because the `impossible` on a pattern match in an anonymous function is not yet implemented. If you're blocked on this, here's a work-around: ```idris import Decidable.Equality...

Thanks! I guess we should decide on whether this is a missing feature, or `\case` is the way to go.

Thanks --- definitely not blocking me, just filing it for future reference.

Not at all! The idea is that a computation returning a serializable value and involving algebraic effects whose parameter and arity types are serializable can be (extensionally) serialized into a...

Non-termination is a computational effect. What kind of strange programming language would include non-termination by default and still consider itself pure?

We have now refactored the IDE protocol representation and its encoding/decoding into a separate [protocols](https://github.com/idris-lang/Idris2/blob/main/ipkg/idris2protocols.ipkg) package. If this Feature Request is still relevant, perhaps this refactoring makes it easier to...

This is really cool and I like the flexibilty this mechanism offers in how it solves the existing issues! Thanks! Two comments: 1. I suggest we use the word `export`...

You might want to draw similarities with, and learn lessons from, the [OCaml extension](https://v2.ocaml.org/manual/bindingops.html) for user-defined binding operations.