Yeah, I think it would be somewhat interesting, but might also have negative side effects of spreading the misconception that constructive code is central to interactive theorem proving.

I've edited the kata after authoring the translation so you might get a description merge conflict when trying to approve the original translation. In that case, you may wish to approve this fork instead.

The Coq version of this kata requires a constructive proof.

Yeah, I think it would be somewhat interesting, but might also have negative side effects of spreading the misconception that constructive code is central to interactive theorem proving.

I see, thanks for explaining, thats a little unfortunate, would be cool to be able to actually test for constructive kata.

This comment is hidden because it contains spoiler information about the solution

This comment is hidden because it contains spoiler information about the solution

which solution?

This comment is hidden because it contains spoiler information about the solution

A good patch is to have

noncomputable theory

open_locale classical

in the header of any Lean kata which is meant to be about "everyday mathematics".

I don't think "learn Lean entirely through exercises on Codewars" is a particularly good life strategy, anymore than it would be for learning other languages. Come ask questions here

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members

or use this website to find reference material

https://leanprover-community.github.io/

I've edited the kata after authoring the translation so you might get a description merge conflict when trying to approve the original translation. In that case, you may wish to approve this fork instead.

Coq Translation Kumited - please accept :-D

This comment is hidden because it contains spoiler information about the solution

This comment is hidden because it contains spoiler information about the solution

I think this would be better with z:\R instead of z:\Z.