Strange bug (it's not a bug)

Stream: lean4

[Pavel Klimov]

inductive A
| a (a : Nat)
| b (a : Nat)
| c (a : Nat)
| d (a : Nat)

abbrev A.cond (b : A) : Prop :=
  match b with
  | .a _a => False
  | .b a => a ≠ 5  -- here <- Invalid pattern: Not enough arguments to `a`; expected 1 explicit argument
  | .c a => a < 5
  | .d _a => False

It is fixed if b param rename into a. There is still bug if you rename inductive type.

[Aaron Liu]

Is it because you have A.cond so the contents of the definition are elaborated having opened the namespace A and so a is being interpreted as A.a?

[Pavel Klimov]

Didn't know that it opens namespace automatically :man_facepalming:. Thanks.