I think it ought to be possible to speed up https://github.com/gallais/agdarsec quite a lot
by not converting a String (aka Haskell's Text) to a List Char but rather processing
the string immediately.

To be able to do that & have the parsers still run at compile time, I need:

• Maybe as a builtin
• uncons : Text -> Maybe (Char, Text) as a primitive
• `length-uncons

After the ring solver has been merged in (#922), we should update the README to demonstrate the new equational reasoning (instead of propositional reasoning) and the solvers.

It will be interesting to implement trees, codata, etc

• Bitbucket: https://bitbucket.org/lambdamix/superspec/issue/27
• Originally Reported By: Ilya Klyuchnikov
• Originally Created At: 2013-08-28T09:02:42.726

Hi,

i think it would be good to update the agda-mode/README.md here in the agda mode in order to specify which commands are shared with Emacs, which commands are only available here in Agda mode, and which commands are only on Emacs and pending integration with Atom.

I could edit the changes if we discuss them in this thread.