chore: make UInt.Lemmas a private import of String.Extra

2026-03-28 07:44:13 +00:00 · 2025-08-25 17:09:39 +02:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -10,7 +10,7 @@ public import Init.Data.ByteArray.Basic
 import all Init.Data.ByteArray.Basic
 public import Init.Data.String.Basic
 import all Init.Data.String.Basic
-public import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Lemmas

 public section