• Now it does say "@nnreal_induction_on" for me, but when I first completed the kata, the test file had "immediate." Maybe if you leave "Example Test Cases" blank it defaults to something that uses "immediate"?

    In any case, it does seem like this issue is now resolved.

  • I think this issue is resolved. I couldn't find any mention of "immediate" anywhere, but I did leave the Example Test Cases blank and they are now filled in.

  • Instead of "immediate", the test file should have "@nnreal_induction_on". Otherwise, nice kata.

  • Okay, thanks for fixing it. The kata itself is really nice, by the way.

  • I updated the sample tests. I don't know why the default one used immediate as the name. The problem was you needed @word_eq_power_tower

  • For some reason the test doesn't work for me even though I was able to submit a successful solution. The output of the test was unknown identifier immediate. When I tried changing immediate to word_eq_power_tower the output was

    type mismatch, term
    has type
      ∀ (a b : ?m_1) (n : ℕ), word a b 1 = a ^ 2 → word a b n = a ^ tower n
    but is expected to have type

    However, as I said, I had no problems attempting or submitting my solution.

  • It would be nice if the initial solution file included the lines

    open tm nvalue lvalue step ty has_type multi
    infix ` ⟶ `:100 := step
    notation `⊢ `:19 t ` :∈ `:20 T := has_type t T
    notation `step_normal_form` := (normal_form step)

    Also, I noticed that the preloaded file contains open nvalue but not open lvalue which doesn't cause any problems, but seems a little weird (and briefly confused me when I was working on solving the kata).

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