Multiple use of variables in syntax quotations

Stream: lean4

[Henrik Böving]

I feel like this code:

def foo : Syntax → Syntax
  | `($x $x) => x
  | _ => sorry

which elaborates to:

def foo : Syntax → Syntax :=
fun x =>
  let discr := x;
  if isOfKind discr `Lean.Parser.Term.app = true then
    let discr_1 := getArg discr 0;
    let discr_2 := getArg discr 1;
    if matchesNull discr_2 1 = true then
      let discr := getArg discr_2 0;
      let x := discr;
      let x := discr_1;
      x
    else
      let discr := getArg discr 1;
      sorryAx Syntax
  else
    let discr := x;
    sorryAx Syntax

Should not be valid? Mentioning the same variable twice inside of a regular pattern also leads to an error. And the elaborated function also basically just overloads things so in big patterns that use many antiquotations stuff like this might end up being hard to debug.

[Notification Bot]

This topic was moved to #lean4-dev > Multiple use of variables in syntax quotations by Leonardo de Moura.