From 7c4c57759dbabfa570ab482b0a2976ce3a6c00a3 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joe@lean-fro.org>
Date: Thu, 11 Jan 2024 10:23:43 -0800
Subject: [PATCH] chore: use more specific import in OfScientific (#3165)

This just removes a spurious import of `Init.Data.Nat`. That's the only
non-aggregating import of that file in Init.
---
 src/Init/Data/OfScientific.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean
index 772ce0b0f9..fd5e46cb39 100644
--- a/src/Init/Data/OfScientific.lean
+++ b/src/Init/Data/OfScientific.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Meta
 import Init.Data.Float
-import Init.Data.Nat
+import Init.Data.Nat.Log2
 
 /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
    Examples: