Instances For
Instances For
Instances For
Instances For
Equations
- Lean.instToFormatName_lean = { format := fun (n : Lean.Name) => Std.Format.text n.toString }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instToFormatProdNameDataValue = { format := fun (x : Lean.Name × Lean.DataValue) => match x with | (n, v) => Std.format n ++ Std.Format.text " := " ++ Std.format v }
Instances For
Equations
- Lean.instToFormatKVMap = { format := Lean.formatKVMap }