matching implicit args

Stream: lean4

[Reid Barton]

Is it possible to pattern match on implicit function arguments with the fun | ... syntax?

[Reid Barton]

e.g. (doesn't work)

theorem f : ∀ {x : ℕ}, x = x := fun
  | {.zero} => rfl
  | {.succ n} => rfl

[Reid Barton]

Oh I understand now what the error message was telling me--use @fun to turn the arguments into regular arguments.