Lean.Meta.CollectFVars

Equations

Equations

Equations

Lean.Meta.removeUnused vars used = do let localInsts ← Lean.Meta.getLocalInstances let lctx ← Lean.getLCtx let discr ← Array.foldrM (fun var x => match x with | (lctx, localInsts, newVars, used) => if Std.RBTree.contains used.fvarSet (Lean.Expr.fvarId! var) = true then do let varType ← Lean.Meta.inferType var let discr ← StateRefT'.run (Lean.Meta.collectUsedFVars varType) used let x : Unit × Lean.CollectFVars.State := discr match x with | (x, used) => pure (lctx, localInsts, Array.push newVars var, used) else pure (Lean.LocalContext.erase lctx (Lean.Expr.fvarId! var), Lean.LocalInstances.erase localInsts (Lean.Expr.fvarId! var), newVars, used)) (lctx, localInsts, #[], used) vars (Array.size vars) let x : Lean.LocalContext × Lean.LocalInstances × Array Lean.Expr × Lean.CollectFVars.State := discr match x with | (lctx, localInsts, newVars, x) => pure (lctx, localInsts, Array.reverse newVars)