getFVars

Stream: lean4

[Marcus Rossel]

The function getMVars returns all mvars contained in a given Expr. Does there exist an analogous function for fvars? The aforementioned getMVars is defined in CollectMVars.lean, and there also exists a CollectFVars.lean, but it doesn't contain a corresponding function. Seeing how getMVars is implemented, would the following be a correct implementation of getFVars?:

def getFVars (e : Expr) : MetaM (Array FVarId) := do
  let (_, s) ← e.collectFVars.run {}
  return s.fvarIds

---

Actually, Mario already posted a simpler version:

def Lean.Expr.getFVars (e : Expr) : Array FVarId :=
  Lean.collectFVars {} e |>.fvarIds