Mhm... That's confusing. I've ran into the same issue with other Kata that use random tests. Is there something that I've done wrong?

Nim tests are broken, as some things have been deprecated.

/workspace/solution_tests.nim(63, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(65, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
/workspace/solution_tests.nim(63, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(66, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
/workspace/solution_tests.nim(70, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(72, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
/workspace/solution_tests.nim(70, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(73, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
Error: execution of an external program failed: '/workspace/tests '

Alright I see. I've yanked the kata at the moment, since this question is from somewhere else, and I might need to get their permission before publishing it.

I think it is, if we define a function in Preloaded that means that if data.nat.pairing is imported then Lean will complain about name collisions. So say

namespace nat

def mkpair (a b : ℕ) := a + b

end nat

in Preloaded, and then in the Test only import Solution and not Preloaded, then check the behaviour of mkpair to check that it is the one from Preloaded and not data.nat.pairing. I think this means that one way or another, the user cannot use mkpair or unpair from data.nat.pairing.

I'm not saying that this is a good idea though!

I suppose it is possible to make it so that people can't use data.nat.pairing, but as imports are transitive in lean, that also means that people can't use anything that imports data.nat.pairing.

Lambda : \Gl, Forall : \all, Exists : \ex. If you press the backslash you should get a list of all the symbols that can be entered.

There are pure ascii equivalents to some of theses (the basic katas can definitely be done in 100% ASCII), but in general it is preferred to use the symbols.

Coming up with names are hard :( Suggestions are welcome for the name.

There is a second part to the question, but as my solution already almost times out for the first part, I didn't add that in.

Questions:

1. TPIL uses a different definition of even and odd with mutual inductive, but I can't seem to get it to behave the way that I want it to. Would that be preferable? In the context of this Kata I don't think there is any benefit to the TPIL version.

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

2. Should maybe one of the first ones, say even_plus_one_is_odd be provided as an example with solution?

3. Are the even_[operation]_odd and odd_[operation]_even ones both needed? It's very easy to go from one to the other.

Hello,

I've written a Lean version of this. Please take a look at it if you can :)