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: