I am always needing sized types I wish they were real
@amy actually while I'm here. what kind of inductive type do you want it for? more specifically does your inductive type X have recursive arguments of type (B -> X) or are they all just shaped mostly like X (up to indices, I guess)
@ionchy https://agda.readthedocs.io/en/latest/language/reflection.html#terms i mostly just want to be able to use traverse for the argument lists lol
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.