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.

Fixed the solution

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

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.

Fixed

It wasn't intentional. It is now fixed.

In the theorem statement of the description, the first two parameters {R : Type*} [comm_ring R] are omitted. Is that intentional?