quote4 match error "resulting term contains metavariable"

Stream: lean4

[David Renshaw]

@Gabriel Ebner : am I doing something wrong here ^ ?

[Gabriel Ebner]

Once you see it, it's obvious. This also works:

def bar (p : Q(Prop)) : TacticM Unit := match p with
  | ~q((($a : Prop)) → ($b : Prop)) => do pure ()
  | _ => pure ()

[Gabriel Ebner]

This is an awkward side effect of the new (a : A) → b syntax for ∀.

[David Renshaw]

thanks!