@[reducible, inline]

abbrev Lean.Meta.Grind.Var : Type

Equations

• Lean.Meta.Grind.Var = Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.FoundVars : Type

Equations

• Lean.Meta.Grind.FoundVars = Std.HashSet Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.VarCollector : Type

Equations

• Lean.Meta.Grind.VarCollector = (Lean.Meta.Grind.FoundVars → Lean.Meta.Grind.FoundVars)

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

Equations

• Lean.Meta.Grind.collectVar x x✝ = Std.HashSet.insert x✝ x

@[instance_reducible]

instance Lean.Meta.Grind.instAndThenVarCollector : AndThen VarCollector

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• s.toArray = (Std.HashSet.toArray s).qsort fun (x1 x2 : Nat) => decide (x1 < x2)

structure Lean.Meta.Grind.VarRename : Type

• map : Std.HashMap Var Var

@[instance_reducible]

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

Equations

• Lean.Meta.Grind.instCoeFunVarRenameForallVar = { coe := fun (s : Lean.Meta.Grind.VarRename) (x : Lean.Meta.Grind.Var) => s.map[x]?.getD 0 }

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

Equations

• One or more equations did not get rendered due to their size.