From e86ff3c76faeb31b7c5eccb4bc6a349ecceba9e2 Mon Sep 17 00:00:00 2001
From: Can Baykar <42147816+canbaykar@users.noreply.github.com>
Date: Sat, 2 May 2026 22:53:06 +0300
Subject: [PATCH] Fix comment formatting

Resolves the error "Incorrect header nesting: expected at most `##` but got `###`". This error prevents LeanPlot from building.
---
 LeanPlot/ToFloat.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanPlot/ToFloat.lean b/LeanPlot/ToFloat.lean
index ae07a9f..853aa51 100644
--- a/LeanPlot/ToFloat.lean
+++ b/LeanPlot/ToFloat.lean
@@ -47,7 +47,7 @@ instance instToFloatInt : ToFloat Int where
 instance [Coe α Float] : ToFloat α where
   toFloat a := ↑a
 
-/-! ### `Rat` instance
+/-! ## `Rat` instance
 
 Lean 4 ships with a rational number type `Rat` in `Init.Data.Rat`.
 The conversion takes the numerator/denominator and performs a floating-point