This Holbert thingy by is pretty neat! Reminds me a bit of Alfa, but more free-form!
I couldn't help myself and defined some dependently typed stuff in it: gist.github.com/brendanzab/1b4. Warning: it's incomplete and probably contains a bunch of mistakes! 😅
Quote Tweet
@brendanzab formalised Martin-Löf type theory in Holbert! Cool!
Show this thread
