Pattern match against implicit arguments

Stream: mathlib4

[Eric Wieser]

Is there any way to name implicit arguments in a pattern match? the context is

import Mathlib.Data.Fin.VecNotation

example {k : ℕ} {x : Fin k → ℕ} : x = x := by
  induction x using Fin.consInduction with
  | h0 => rfl
  | h x₀ x ih => rfl  -- how do I name `n` here? Why is `k` still around?

[James Gallicchio]

You can use @s in patterns now -- so @h n x0 x ih should work

[James Gallicchio]

as for why k is still around, I have no idea. maybe induction is now smarter about not generalizing stuff when it doesn't have to? unsure

[Mario Carneiro]

why wouldn't k still be around? AFAIK induction never removes the "original" variables from the context unless it is reverting them for generalizing

[Eric Wieser]

It always removed them in Lean3

[Eric Wieser]

Because they stop existing anywhere else in the context, so in a proof they become useless