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

Follow

ASTs are finitary, after all

Sign in to participate in the conversation
types.pl

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