👩💻 Join our community of thousands of amazing developers!
.highlight .err { background-color: inherit; } This post is inspired by this thread from the Agda mailing list. Because Agda treats Size like a first-class type, there’s quite a bit of freedom in how you get to use it. This makes it a bit unclear where you should start: should Size be a parameter or an index in your type? What sizes should the constructors’ recursive arguments’ and return types have? Here are two options that are usually used (and one that doesn’t work.) The recommende...