Explicit name for prop `x = (a,b)` in `match ... | x@(a,b)`

Stream: general

[nrs]

Can I give an explicit name to the proposition arising from match ... with | x@(a, b), ... => ... | ..., y@(c, d) => ... stating that x = (a, b) or y = (c, d) in term mode? Instead of entering tactic mode to rename_i afterwards

[Mario Carneiro]

match h : ...

[nrs]

hm, but does that not only work with matches of the form x@(a,b) => ...? sorry the title is a bit misleading, could not fit enough examples

[Mario Carneiro]

no?

[Kyle Miller]

(an #mwe with a representative example would make this easy to answer)

[nrs]

For instance, this will introduce two inaccessible names:

def prodmatch (prod : Nat × Unit × (Nat ⊕ Nat) × (Unit × Nat)) : Nat :=
  match ha : prod with
  | x@⟨nat, u, sum, y@⟨ub, natb⟩⟩ => _

[Kyle Miller]

def prodmatch (prod : Nat × Unit × (Nat ⊕ Nat) × (Unit × Nat)) : Nat :=
  match prod with
  | x@hx:⟨nat, u, sum, y@hy:⟨ub, natb⟩⟩ => _

[nrs]

very cool! thanks a lot!!

[Frederick Pu]

sorry to intrude but what is this @ operator do?

[Mario Carneiro]

it "names" the subpattern

[Mario Carneiro]

so inside the match x will be bound to the original expression and y will be bound to the Unit × Nat subterm

[Frederick Pu]

k cool