Stefan Höck

You are right, of course. I will look into this and try to indeed break things up.

Yes, the representation we use for sum types leads to a quadratic number of nested data constructors: ```idris Z v S(Z v) S(S(Z v)) .... ``` Type-checking these will therefore...

Thanks. Can you ping me, once the PR is ready for merging?

I'd like to take this whole thing a bit further, because this is also related to an issue in the todo list: How should we handle multi-ipkg projects in general?...

> idris2-lsp currently index packages in ~/.idris2/xxxx (I think it's hard coded). It uses similar/same logic as --find-ipkg to get dependencies. Packages have to be installed with `install-src` for go-to-declaration...

> Sorry, I was using an old version of lsp and pack. Now that I upgraded both, it works. > > Slight problem: `pack install-app lsp` doesn't create `~/.pack/bin/idris2-lsp`. I...

This was not intentional. This project is still very young, and a lot of stuff is still missing. There are several options here: Use `Web.Raw.Dom.createElement` or `Web.Raw.Dom.createElement'` to create a...

Could you please write a short spec describing the order of commands and arguments pack should accept? In order to make this happen we not only need to change how...

I submitted a PR adding a new `--cg` command-line option. The default codegen to use can also be specified in the `pack.toml` files. However, I'm not sure I follow your...

I'm truly sorry I missed this question. Right now, there seems no easy way to do this other than using `unsafePerformIO`. I'll have to think some more about how easy...