Made a Matrix room for my programming language Pikelet at! Come hang out if you want to chat about Pikelet, dependent types, systems programming, and flights of fancy about structured editing that I'll probably never get around to finishing…

Mixing Ltac and Gallina for Fun and Benefits

This is the latest blogpost on my website, and it is the second blogpost on Ltac on my website. Hope you find it interesting!

(Some familiarity with Coq is required, unfortunately.)

@brendanzab laying out a lovely, no mess no fuss, story of needing, learning about and making important use of dependant types at Compose Melbourne. We’re so lucky you’re doing your thing, Brendan :)


Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!