Philippa Cowderoy @flippac@types.pl

Turns out breaking tell constraints into tiny pieces is a much bigger pain in the arse than doing it for ask ones because you're not supposed to know anything about what you're writing into

I can't help thinking that whatever else is going on, social media has just inherently become more antisocial for me over the last decade.

I'm not saying I can't nerd out on here, but I don't know if making actual friends without f2f contact is going to be much of a thing.

A lot of that is, tbh, about privacy: the granularity of locking posts on some of the older sites is clearly not compatible with Mastodon. It's always been necessary to have room to be more honest than one can afford in front of the modern internet.

I am once again considering bolting on vectors to my toy logic language stuff so I can write zipWithN (with lengths having to match) once and for all...

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.