Elaboration of swift notation

Stream: lean4 dev

[felko]

Hello, I am trying to fix this issue https://github.com/leanprover/lean4/issues/2626
Since I am new to the lean codebase, I was wondering where should I start looking.
As mentionned in the issue, I was pretty sure the bug was coming from Lean.Elab.PatternVar but inserting a few dbg_trace there, I am reconsidering this because none of the dbg_trace are triggered.
I was wondering specifically where was located the logic of turning swift notation in patterns (| .ctor ... =>) into qualified constructor patterns.