source
@[reducible, inline]
abbrev Lean.Meta.Grind.Var :
Type
Equations

- Lean.Meta.Grind.Var = Nat

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.FoundVars :
Type
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.VarCollector :
Type
Equations

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

Instances For

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

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

Instances For

source
instance Lean.Meta.Grind.instAndThenVarCollector :
AndThen VarCollector
Equations

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

source
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.

Instances For

source
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)

Instances For

source
structure Lean.Meta.Grind.VarRename :
Type

- map : Std.HashMap Var Var

Instances For

source
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 }

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

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

Instances For