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

Sign in to participate in the conversation

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