feat: expose getPatternVars

src/Lean/Elab/Match.lean

@@ -405,7 +405,7 @@ match (stx.getArg 0).isNameLit? with
 | some val => nameToPattern val
 | none     => throwIllFormedSyntax
 
-private partial def collect : Syntax → M Syntax
+partial def collect : Syntax → M Syntax
 | stx@(Syntax.node k args) => withRef stx $ withFreshMacroScope $
   if k == `Lean.Parser.Term.app then do
     processCtorApp collect stx
@@ -496,6 +496,12 @@ private def collectPatternVars (alt : MatchAltView) : TermElabM (Array PatternVa
 (alt, s) ← (CollectPatternVars.main alt).run {};
 pure (s.vars, alt)
 
+/- Return the pattern variables in the given pattern.
+  Remark: this method is not used here, but in other macros (e.g., at `Do.lean`). -/
+def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do
+(_, s) ← (CollectPatternVars.collect patternStx).run {};
+pure s.vars
+
 /- We convert the collected `PatternVar`s intro `PatternVarDecl` -/
 inductive PatternVarDecl
 /- For `anonymousVar`, we create both a metavariable and a free variable. The free variable is used as an assignment for the metavariable