FYI you can ask this on CW gitter
I don't think so?
Maybe the use of lemmas in Data.Nat.Properties sould be prohibited?
This comment is hidden because it contains spoiler information about the solution
Indeed, a very satisfying kata when completed ! I'm new to Kotlin, it's so powerful.
If that may help anyone, it took me about 5 minutes of googling to get a slight hint, and I tried a bit, and... voilà
Given that the author hasn't logged in for 2 years, and first I reported this 4 years ago I decided to fix the types myself.
Approved your one. Looks good!
Yeah, I get that, I stumbled across this translation after writing my own here. I wasn't sure if I should look at tidying this up since its been 4 months or publish a separate one. (I thought CW was supposed to warn me if I tried to create another translation for one that was already in progress. Well thats what the wiki said anyway)
I was pondering about program correctness too, and I came to the conslusion that it's a subjective term, so we can only pove that our program behaves according to a formal specification but can never prove that "its bug free" whatever that means.
So my thinking is that there is no such thing as proof of correctness, until we can formalize "correctness" which we can't.