finally bit the bullet, sat down, and dug up my old custom iosevka config. there's so many nice new calts available
anyway, iosevka term custom™ is ready, time to work through Programming Language Foundations in Agda :D
Conversation
have any of you done PLFA, how do you like it
feels like it's what I need to do to not feel so horribly at sea when working on typecheckers, especially as i near the point where i start working on my first real language now that I have an idea (or two!) of what i want
1
1
if i ever cook up a core calculus of my own instead of stealing one from a paper you bet I'm going to verify it first and not sink mountains of cost into a frontend based on it while being aware there's a vanishingly small chance the core TT is unrepairably broken
1
1
I should probably do this. 😰
1
1
If only doing anything with proofs about variable binding and dependent types wasn't such a pain (so I hear).