Naming equality hypothesis in match branch

Stream: lean4

[Adam Topaz]

Consider the following:

def test : List Nat → Unit
  | [] => .unit
  | t@(x :: xs) =>
    /-
    t: List Nat
    x: Nat
    xs: List Nat
    h✝: t = x :: xs
    ⊢ Unit
    -/
    sorry

In the second branch, t@(x :: xs), do we have some convenient way to name the hypothesis h✝: t = x :: xs?

[Shreyas Srinivas]

yes we do

[Shreyas Srinivas]

def test (k : List Nat) : Unit :=
  match h : k with
  | [] => .unit
  | t@(x :: xs) =>
    /-
    t: List Nat
    x: Nat
    xs: List Nat
    h✝: t = x :: xs
    ⊢ Unit
    -/
    sorry

[Adam Topaz]

no, that doesn't answer my actual question.

[Adam Topaz]

That gives a hypothesis h : k = x :: xs, not t = x :: xs.

[Shreyas Srinivas]

Oh okay. Apologies for misunderstanding the question

[Eric Wieser]

I think the answer is no

[Eric Wieser]

Oh, the comment is wrong!

def test : List Nat → Unit
  | [] => .unit
  | t@ht : (x :: xs) =>
    sorry

[Adam Topaz]

aha!

[Eric Wieser]

(guessed from here)

[Eric Wieser]

Comment is fixed in lean4#3073

[Kevin Buzzard]

I've seen plenty of this but this is the first time I've seen th@t. Oh, sorry, t@ht.

[Adam Topaz]

I'm happy such a syntax exists, but my first guess would have been ht:t@(x :: xs).

[Utensil Song]

What does @ mean in general? I can't really parse it with : in my mental model :joy:

[Yury G. Kudryashov]

BTW, what's the rationale behind these equalities no longer being definitional? In Lean 3, it was possible to use t as a short name for x :: xs.

[Thomas Murrills]

Utensil Song said:

What does @ mean in general? I can't really parse it with : in my mental model :joy:

In patterns, @ lets you name terms while still destructuring them: | a@(x :: xs) => body matches x :: xs and binds x and xs as usual, but also gives the whole thing the name a.

That’s why this syntax is weird: you’d expect t@ht : x :: xs to name…just ht, I suppose? Even t@(ht : x :: xs) would look wrong, since t is the name for x :: xs, not some ht. (And ht doesn’t really have type x :: xs, of course, so we’re using a lot of notation differently here.)