Fix comment formatting

[canbaykar]

Resolves the error Incorrect header nesting: expected at most '##' but got '###'. This error prevents LeanPlot from building. Here is the full error message I get from the line import LeanPlot.API:

`c:\Users\Togan\.elan\toolchains\leanprover--lean4---v4.29.0-rc6\bin\lake.exe setup-file C:\Users\Togan\Documents\Projects\Lean with mathlib\Lean with mathlib\example3.lean -` failed:

stderr:
⚠ [16/29] Replayed LeanPlot.Axis
warning: LeanPlot/Axis.lean:5:20: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`AxisProps`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`AxisProps`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:5:45: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`ProofWidgets.Recharts.AxisProps`
  • {̲n̲a̲m̲e̲}̲`ProofWidgets.Recharts.AxisProps`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`ProofWidgets.Recharts.AxisProps`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:6:17: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`label?`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`label?`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:9:15: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`XAxis`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`XAxis`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:9:27: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`YAxis`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`YAxis`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:10:30: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"XAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"XAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"XAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"XAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"XAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"XAxis"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"XAxis"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:10:44: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"YAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"YAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"YAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"YAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"YAxis"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"YAxis"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"YAxis"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:20:2: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`none`
  • {̲n̲a̲m̲e̲}̲`none`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`none`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:22:24: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`[lo, hi]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`[lo, hi]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`[lo, hi]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`[lo, hi]`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`[lo, hi]`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:22:62: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`none`
  • {̲n̲a̲m̲e̲}̲`none`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`none`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:25:11: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲k̲w̲ ̲(̲o̲f̲ ̲:̲=̲ ̲L̲e̲a̲n̲.̲J̲s̲o̲n̲.̲j̲s̲o̲n̲T̲r̲u̲e̲)̲}̲`true` (in `json`)
  • {̲k̲w̲ ̲(̲o̲f̲ ̲:̲=̲ ̲L̲e̲a̲n̲.̲r̲e̲d̲u̲c̲e̲C̲m̲d̲)̲}̲`true` (in `command`)
  • {̲l̲e̲a̲n̲}̲`true`
  • {̲n̲a̲m̲e̲}̲`true`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`true`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`true`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:26:30: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲k̲w̲ ̲(̲o̲f̲ ̲:̲=̲ ̲L̲e̲a̲n̲.̲J̲s̲o̲n̲.̲j̲s̲o̲n̲F̲a̲l̲s̲e̲)̲}̲`false` (in `json`)
  • {̲l̲e̲a̲n̲}̲`false`
  • {̲n̲a̲m̲e̲}̲`false`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`false`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`false`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:29:2: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`category`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`category`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:32:5: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Option Json`
  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`Option Json`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`Option Json`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`Option Json`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`Option Json`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Option Json`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:32:31: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Option String`
  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`Option String`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`Option String`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`Option String`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`Option String`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Option String`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:33:40: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`angle`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`angle`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:33:50: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`position`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`position`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:33:63: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`dx`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`dx`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:35:15: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Json.str "my-label"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`Json.str "my-label"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`Json.str "my-label"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`Json.str "my-label"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Json.str "my-label"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:17:0: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`ProofWidgets.Recharts.AxisProps`
  • {̲n̲a̲m̲e̲}̲`ProofWidgets.Recharts.AxisProps`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`ProofWidgets.Recharts.AxisProps`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Axis.lean:17:48: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`label?`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`label?`
    to mark the code as literal text and disable suggestions
⚠ [17/29] Replayed LeanPlot.Legend
warning: LeanPlot/Legend.lean:7:46: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`Legend`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Legend`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:19:65: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"vertical"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"vertical"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"vertical"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"vertical"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"vertical"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"vertical"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"vertical"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:19:81: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"horizontal"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"horizontal"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"horizontal"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"horizontal"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"horizontal"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"horizontal"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"horizontal"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:19:115: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`layout`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`layout`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:21:48: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"top"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"top"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"top"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"top"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"top"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"top"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"top"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:21:57: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"middle"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"middle"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"middle"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"middle"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"middle"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"middle"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"middle"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:21:69: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"bottom"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"bottom"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"bottom"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"bottom"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"bottom"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"bottom"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"bottom"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:23:46: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"left"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"left"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"left"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"left"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"left"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"left"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"left"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:23:56: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"center"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"center"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"center"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"center"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"center"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"center"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"center"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:23:68: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`"right"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`"right"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`"right"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲j̲s̲o̲n̲}̲`"right"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`"right"`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`"right"`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`"right"`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Legend.lean:32:14: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Legend`
  • {̲n̲a̲m̲e̲}̲`Legend`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Legend`
    to mark the code as literal text and disable suggestions
ℹ [18/29] Replayed LeanPlot.Palette
info: LeanPlot/Palette.lean:111:0: true
info: LeanPlot/Palette.lean:112:0: true
ℹ [21/29] Replayed LeanPlot.Metaprogramming
info: LeanPlot/Metaprogramming.lean:251:0: #["time"]
info: LeanPlot/Metaprogramming.lean:252:0: ("time", "f(time)")
info: LeanPlot/Metaprogramming.lean:254:0: #["x", "y", "x_2"]
info: LeanPlot/Metaprogramming.lean:255:0: ("x", "y")
info: LeanPlot/Metaprogramming.lean:258:0: #["x", "y", "x_2", "z", "x_3"]
info: LeanPlot/Metaprogramming.lean:259:0: #["time", "time_2", "velocity"]
info: LeanPlot/Metaprogramming.lean:262:0: #["time"]
info: LeanPlot/Metaprogramming.lean:263:0: ("time", "f(time)")
info: LeanPlot/Metaprogramming.lean:264:0: #["a", "a_2", "b"]
⚠ [22/29] Replayed LeanPlot.Constants
warning: LeanPlot/Constants.lean:9:41: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`lineChart`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`lineChart`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Constants.lean:9:53: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`scatterChart`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`scatterChart`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Constants.lean:12:42: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`lineChart`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`lineChart`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Constants.lean:12:54: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`scatterChart`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`scatterChart`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/Constants.lean:17:32: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
✖ [24/29] Building LeanPlot.ToFloat (927ms)
trace: .> LEAN_PATH=C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\subverso\.lake\build\lib\lean;C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\MD4Lean\.lake\build\lib\lean;C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\verso\.lake\build\lib\lean;C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\LeanPlot\.lake\build\lib\lean;C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\build\lib\lean c:\Users\Togan\.elan\toolchains\leanprover--lean4---v4.29.0-rc6\bin\lean.exe C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\LeanPlot\LeanPlot\ToFloat.lean -o C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\LeanPlot\.lake\build\lib\lean\LeanPlot\ToFloat.olean -i C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\LeanPlot\.lake\build\lib\lean\LeanPlot\ToFloat.ilean -c C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\LeanPlot\.lake\build\ir\LeanPlot\ToFloat.c --setup C:\Users\Togan\Documents\Projects\Lean with mathlib\.lake\packages\LeanPlot\.lake\build\ir\LeanPlot\ToFloat.setup.json --json
warning: LeanPlot/ToFloat.lean:1:6: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`ToFloat`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`ToFloat`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:2:74: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:4:36: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:5:4: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`[ToFloat]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`[ToFloat]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`[ToFloat]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`[ToFloat]`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`[ToFloat]`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:8:6: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲g̲i̲v̲e̲n̲}̲`ToFloat`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`ToFloat`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:11:13: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:12:68: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:13:38: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`[ToFloat]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`[ToFloat]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`[ToFloat]`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`[ToFloat]`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`[ToFloat]`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:24:27: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:19:42: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:20:28: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Int`
  • {̲n̲a̲m̲e̲}̲`Int`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Int`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:20:37: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Nat`
  • {̲n̲a̲m̲e̲}̲`Nat`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Nat`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:22:10: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Float`
  • {̲n̲a̲m̲e̲}̲`Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:29:36: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`toFloat a`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`toFloat a`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:29:59: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`ToFloat.toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`ToFloat.toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`ToFloat.toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`ToFloat.toFloat a`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`ToFloat.toFloat a`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`ToFloat.toFloat a`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:44:4: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Coe α Float`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`Coe α Float`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`Coe α Float`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`Coe α Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Coe α Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:45:28: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`instToFloatFloat`
  • {̲n̲a̲m̲e̲}̲`instToFloatFloat`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`instToFloatFloat`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:45:55: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Coe α Float`
  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`Coe α Float`
  • {̲s̲y̲n̲t̲a̲x̲ ̲g̲r̲i̲n̲d̲_̲r̲e̲f̲}̲`Coe α Float`
  • {̲s̲y̲n̲t̲a̲x̲ ̲t̲e̲r̲m̲}̲`Coe α Float`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Coe α Float`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:46:6: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Subsingleton`
  • {̲n̲a̲m̲e̲}̲`Subsingleton`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Subsingleton`
    to mark the code as literal text and disable suggestions
error: LeanPlot/ToFloat.lean:50:4: Incorrect header nesting: expected at most `##` but got `###`
warning: LeanPlot/ToFloat.lean:52:41: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲l̲e̲a̲n̲}̲`Rat`
  • {̲n̲a̲m̲e̲}̲`Rat`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Rat`
    to mark the code as literal text and disable suggestions
warning: LeanPlot/ToFloat.lean:52:50: Code element could be more specific.

Hint: Insert a role to document it:
  • {̲m̲o̲d̲u̲l̲e̲}̲`Init.Data.Rat`
  • Use the `lit` role:
    {̲l̲i̲t̲}̲`Init.Data.Rat`
    to mark the code as literal text and disable suggestions
error: Lean exited with code 1
Some required targets logged failures:
- LeanPlot.ToFloat
Failed to build module dependencies.

Here is my lakefile when I encountered the build error:

name = "Lean with mathlib"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["«Lean with mathlib»"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "LeanPlot"
git = "https://github.com/alok/LeanPlot"
rev = "main"

[[lean_lib]]
name = "«Lean with mathlib»"

The error resolved when I changed the ## to ###.

[alok]

Thanks for the focused fix. I reproduced the Verso/SubVerso header-nesting failure and verified this one-line change with lake build LeanPlot.ToFloat, the full lake build, and the documentation build on the current Lean 4.32 toolchain line. Merging this separately so your fix and attribution remain intact.