Alex Gryzlov

There's an Idris implementation of fresh lists at https://github.com/ohad/collie/tree/main/src/Data/List

TBH I haven't tried recompiling this branch for a few months, as Idris2 is currently a bit of a moving target. However given that @gallais is a team member now,...

Ah, if it's down to just a performance issue, that sounds pretty good, given that Edwin lately seems to prioritize those :)

I've updated the examples but still none of them work except `Ambig`, somehow. I wonder what it is getting stuck at now?

What's curious is that (at least for `NList` and `Parentheses`) if you comment out the test cases and run the corresponding parse commands in the REPL manually, you get the...

@gallais have you had any progress on debugging this, or should I take a look?

I made a `parseMaybe` function for internal use which is very similar to `parse`, only returning `Just`/`Nothing` instead of `Singleton`/`Void`. Not sure about returning `List` though. Also what do you...

We currently have `parseMaybe`, `parseType`, `parseResults` and `parseResult` - do you have any other useful variations in mind, or should we close this?

Nix sometimes behaves mysteriously when used to build Idris projects - we've repeatedly ran into a situation where the build was failing with something like `Nat not found` or `Vect...

Note that Idris1 already supports this with `--mkdoc` cmdline option, but it is broken due to https://github.com/idris-lang/Idris-dev/issues/2161