codewars / exercism

Stream: lean4

[Nicolas Rolland]

The kata at codewars are in Lean3. Is there any other exercice platform which has Lean4 ?
exercism.org, which has the advantage of using local language installation thus interactive support, has no Lean4 exercice, unfortunately.

[Eric Wieser]

Note there is a #Codewars stream; I think requesting Lean 4 support would be totally reasonable, although we might want to save our "ask codewars nicely" budget until things like the Std4/Mathlib4 split have stabilized a little more.

[Adolfo Neto]

It would be great to have a Lean track on Exercism! Do we have a unit testing framework for Lean?

[Schrodinger ZHU Yifan]

yes

[Schrodinger ZHU Yifan]

there is a lib called nest by @Henrik Böving