@[reducible, inline]

abbrev Lean.Meta.Grind.Var : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.FoundVars : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.VarCollector : Type

def Lean.Meta.Grind.collectVar (x : Var) : VarCollector

instance Lean.Meta.Grind.instAndThenVarCollector : AndThen VarCollector

def Lean.Meta.Grind.collectMapVars {α : Type u_1} {Expr : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α Expr) (k : α → VarCollector) : VarCollector

def Lean.Meta.Grind.FoundVars.toArray (s : FoundVars) : Array Var

structure Lean.Meta.Grind.VarRename : Type

• map : Std.HashMap Var Var

instance Lean.Meta.Grind.instCoeFunVarRenameForallVar : CoeFun VarRename fun (x : VarRename) => Var → Var

def Lean.Meta.Grind.mkVarRename (new2old : Array Var) : VarRename