Philippa Cowderoy @flippac@types.pl

The very bad solution is to check if I got the exact same input state back - such efficiency!

I think what I want to do for many reasons is build a little consumption machine and rework everything in terms of it

Started hacking up a parsing applicative in Agda as an exercise, have got most of it sorted but run smack into an issue I know a very bad solution to and some more sensible approaches

Haskell wouldn't do this one to me, but it'd screw me over when I used it instead: trying a non-consuming parser many times

$\mathrm{this} \in \mathrm{shitpost}$

$shitpost = 💩​✉️​$

I'm still very much in beginner mode when it comes to Agda. On the bright side this means emacs doesn't get a chance to piss me off.

Meanwhile I'm in a whole universe of pain, but it'll get me a twofer of life being easier later on so I guess I'll take it.

LaTeX support and no preview option I can find doesn't seem great?

Oh look, a world. I'm sure something can infer my response for me.