I've been writing programs in Agda for years (since when they didn't have sized types or cubical theory) but I never heard "Walther recursion" before. If this i

I've been writing programs in Agda for years (since when they didn't have sized types or cubical theory) but I never heard "Walther recursion" before. If this is your day 0 I doubt you need to know about it to understand the language.