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.

Resolved

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
  word_eq_power_tower
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
  SUBMISSION

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).