Find open statements in syntax

Stream: Is there code for X?

[Michael Rothgang]

Inspired by this PR review comment: I wrote a function

/-- If `stx` is syntax describing an `open` command, `extractOpenNames stx`
returns an array of the syntax corresponding to the opened names,
omitting any renamed or hidden items. -/
def extractOpenNames : Syntax → Array Syntax
  | `(command|open $args*)             => args
-- further cases omitted

and @Damiano Testa suspected it already exists. Neither he nor I can find it, though: if you know where it is, that would be appreciated!