def Lean.Meta.Grind.Arith.mkLetOfMap {α : Type u_1} {x✝ : Hashable α} {x✝¹ : BEq α} (m : Std.HashMap α Expr) (e : Expr) (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr

Equations

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