fix: mark ByteArray.Iterator Inhabited instance as noncomputable

The Iterator structure has a custom SizeOf instance that depends on runtime
array size, making the Inhabited instance noncomputable. This change explicitly
marks it as such and adds a comment explaining why.

Related: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Compiler.20error.20with.20sizeOf/with/561532734

Co-authored-by: nomeata <[email protected]>

Author: Copilot

src/Init/Data/ByteArray/Basic.lean

@@ -338,9 +338,12 @@ structure Iterator where
   `Iterator.next` when `Iterator.atEnd` is true. If the position is not valid, then the
   current byte is `(default : UInt8)`. -/
   idx : Nat
-  deriving Inhabited
 set_option doc.verso true
 
+/-- Noncomputable because it depends on the custom `SizeOf` instance which uses runtime array size. -/
+noncomputable instance : Inhabited Iterator where
+  default := ⟨default, default⟩
+
 /-- Creates an iterator at the beginning of an array. -/
 def mkIterator (arr : ByteArray) : Iterator :=
   ⟨arr, 0⟩