How can it throw an `unknown identifier`?

Stream: general

[Paweł Balawender]

Hey! I was coding in Lean and suddenly got stuck on an unknown identifier error that for me completely doesn't make a sense. I minimized the example and put it here : live lean , but I also attach the code here. Do I not understand something fundamental, or the error message is misleading?

universe u

variable {num str: Type u}
variable [Zero num] [One num] [Add num] [LE num]
variable (seq : num -> str -> num)

structure VTC0 where
  b3  : ∀ x : num, x + 0 = x
  seq_ax : ∀ (x : num) (Z : str) (y : num),
    y = seq x Z ↔ True

variable (h : VTC0 seq)
#check h
#check VTC0.b3 h
#check h.b3

theorem leq_refl : ∀ x : num, x <= x := by
  intro x
  apply h -- here, unknown identifier 'h'

[Aaron Liu]

section variables with explicit binders are not included in theorems unless the statement contains the variable

[Markus Himmel]

See this paragraph from the reference (emphasis mine):

Section variables are parameters that are automatically added to declarations that mention them. This occurs whether or not the option autoImplicit is true. Section variables may be implicit, strict implicit, or explicit; instance implicit section variables are treated specially.

When the name of a section variable is encountered in a non-theorem declaration, it is added as a parameter. Any instance implicit section variables that mention the variable are also added. If any of the variables that were added depend on other variables, then those variables are added as well; this process is iterated until no more dependencies remain. All section variables are added in the order in which they are declared, before all other parameters. Section variables are added only when they occur in the statement of a theorem. Otherwise, modifying the proof of a theorem could change its statement if the proof term made use of a section variable.

[Paweł Balawender]

Wow! Thank you @Aaron Liu and @Markus Himmel , section variables is the keyword indeed