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