possible hygenic name issue in pattern matching

Stream: lean4

[Arien Malec]

In:

theorem foo: ∀ (x : Nat), x = 0 → x ≠ 1
| x => by sorry

The tactic state is:

x✝: Nat
x: Nat := x✝

rather than x: Nat

The workaround is to avoid pattern matching

theorem foo: ∀ (x : Nat), x = 0 → x ≠ 1 :=
  fun x => by sorry

Admittedly the pattern matching version is a stranger way to spell ∀x than fun x => but this bit me in a mathlib port.

[James Gallicchio]

I'm surprised mathlib doesn't lint for single-pattern matches, since it's never really what you want :joy:

[Floris van Doorn]

I'm curious: in what way does this lead to problems?

[Floris van Doorn]

I guess you're using a tactic that doesn't expect a let binding?

[Reid Barton]

I'm also curious why it happens at all

[Reid Barton]

I mean if there was more than one branch, then the original variable would not survive, right?

[Reid Barton]

Or if we match on a pair?

[Arien Malec]

Floris van Doorn said:

I'm curious: in what way does this lead to problems?

It caused hygienic name issues after a cases' x with x x

[Arien Malec]

The issues were in star_rmatch_iff in !4#2306 if you are curious. The new x created by cases' is completely dissociated from the let binding.