Jan de Muijnck-Hughes

A good action point from this issue would be to have some documentation contributed to the language reference, and beginner tutorial, to clarify matters.

@Sintrastes I had a quick play with your code a managed to get a working solution, the code is at the end. Essentially, I made the auto implicit an explicit...

Sorry, I do not follow the question?

None of the parser in this package are feature complete (it says as much in the projects README). More so I am fully aware of their limitations. Special characters are...

Sorry, I've not been around to address issues. I havn't really checked this project, or charm-crypto for many years. If you can fix it great. Otherwise, I do not have...

From a quick look over the source, I think the issue here is that Idris2 generates a `ttc` file with the file's basename. Thus, when given a literate idris file...

This looks very interesting, thanks! I was wondering if the named should refer to TT more than idris, especially as you are going from TT rather than Idris.

> was thinking of it as "Idris Core" by analogy to GHC Core. Funnily enough that *is* the correct analogy you are going for, and fortunately for Idris the core...

We must also look at how it works in Idris1 where you can use the `--highlight` flag dump an SExpr containing highlighting information. There is a tool [`idrishl`](https://github.com/david-christiansen/idris-code-highlighter) which can...

I would argue that lambda case is a good way to go. Especially, if it is well documented.