I think over the winter break I actually do want to try to disable the infinite size in Agda's source code and then play around with sized types that don't use it
There's a bunch of good examples to try out but they're scattered all throughout the various github issues on sized typese


ASTs are finitary, after all

Sign in to participate in the conversation

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