Needs an implicit parameter

[VhRvo]

The next few lines show that there should be an implicit parameter

[Kha]

Why? The parameter is inserted automatically. And I'm not sure why the "next few lines" are supposed to show me.

[VhRvo]

I am sorry for using the confusing phrase "next few lines".

As a newbie, when I was learning Lean4, I wrote code at random and wrote something like this:

universe u
variable (α : Type u)

namespace Hidden
inductive List (α : Type u) where
  | nil  : List α
  | cons : α → List α → List α

namespace List
-- def append (as bs : List α) : List α :=
def append {α : Type u} (as bs : List α) : List α :=
   match as with
   | nil       => bs
   | cons a as => cons a (append as bs)

theorem nil_append (as : List α) : append nil as = as :=
  rfl

end List
end Hidden

At this point, the parameter is not automatically inserted. It's a surprise to me. So I think it's better to write this code "explicitly" for newbie's learning.