re: CPP 2021 

This is just a longwinded way of saying tbh

Show thread

This has only happened twice so idk if it counts as a pattern
Pattern matching without K and Definitional Proof-Irrelevance without K
For someone who is on this is ironic

Show thread

Given that it only takes six people tooting a hashtag to get it trending on this tiny instance I'm appalled I haven't managed to get trending yet

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.